PartialFunctions(S, T) == UNION { [x -> T] : x \in SUBSET S}
DictionaryType == PartialFunctions(STRING,STRING)
\* TLC is not able to check if a certain function is in the DictionaryType
\* ASSUME [key1 |-> "val1", key2 |-> "val2", key3 |-> "val3"] \in DictionaryType
\* PartialFunctions should be used if S and T are finite (and small)
inDictionaryType(f) ==
/\ DOMAIN(f) \subseteq STRING
/\ \A x \in DOMAIN f: f[x] \in STRING
ASSUME inDictionaryType([key1 |-> "val1", key2 |-> "val2", key3 |-> "val3"])
\* An alternative approach is to define the dictionary using sets of pairs instead of functions
DictionaryType2 == { f \in SUBSET (STRING \times STRING): \A <<a,b>> \in f,<<c,d>> \in f: a=c => b = d }
ASSUME {<<"key1","val1">>, <<"key2","val2">>, <<"key3", "val3">>} \in DictionaryType2
ASSUME {<<"key1","val1">>, <<"key1","val2">>} \notin DictionaryType2
GetValue(f,x) == (CHOOSE pair \in f: pair[1] = x)[2]
ASSUME GetValue({<<"key1","val1">>, <<"key2","val2">>, <<"key3", "val3">>}, "key2") = "val2"
=============================================================================