Dictionary type

[Paul Eipper <lkra...@xxxxxxxxx>]

Hello all,

How would one go about specifying a dictionary type, such that all
keys and values are strings?

In the spec summary we have for the Record definition:
[h1 : S1,...,hn : Sn] [Set of all records with hi component in Si]

What is the Set of all records *with arbitrary number of fields* with
components in S?

In other words, how to define Dictionary such that:
[key1 |-> "value1", ..., keyN |-> "valueN"] \in Dictionary ?

thanks,
--
Paul Eipper