4.9.9 Set (accumulative)

A set over a domain. Different lattices depending on the domain, which can be:

1. a finite domain of constants
2. integer
3. a tuple of which all projections are finite domains of constants

4.9.9.1 Set generator expressions

Values of accumulative sets over tuples of finite domains of constants (b) can be specified using set generator expressions. Set generator expressions are explained in the previous section for intersective sets.

4.9.9.2 Top value

1. empty set
2. empty set
3. empty set

4.9.9.3 Bottom value

1. the full set (containing all constants in the domain)
2. the set of all integers
3. the full set (containing all tuples in the domain)

4.9.9.4 Greatest lower bound operation

1. set union
2. set union
3. set union

4.9.9.5 Example

Here is an example accumulative set type definition with domain type ref("type"):

     deftype "set" ref("type")