An ASM macro language for sets
P Kutter · Repository for Publications and Research Data (ETH Zurich) · 1998
In the paper I introduce a macro language which allows to use in Gurevich's Abstract State Machines (ASMs) directly the set notation. I define families of sets, a language of set terms (union, intersection, instances of families, Cartesian products), their semantics if they appear in transition rules (extension of family-instances, vary over set terms, assignments of set terms to family-instances), and their semantics in boolean terms like set-inclusion and element-of relation. The semantics is given in terms of ASM-rules. The idea of this macro language is to allow to manipulate sets directly without changing the semantics of ASMs [Gur95]. An integration of sets in the semantics of ASMs has been formalized in [BGS97]. The presented macros have shown to be very useful in the specification of SQL [DiF97]. In ASMs the state is an algebra which has one carrier set, the so called SuperUniverse. Subsets of the super universe, so called universes, are represented by their characteristic f...