### Set annotations:

The set annotations work on pointer sets (i.e. ptrset types), which contain void * elements.

{colorizer-syntax:C#}

ptrset set_singleton(void* x)

Represents a set which contains a single element

*x*.

>

**{ x }**
ptrset set_difference(ptrset X, ptrset Y)

Represents the a pointer set containing all elements of pointer set

*X*, which are not contained in pointer set

*Y*.

>

**X ∖ Y**
ptrset set_union(ptrset X, ptrsetY)

Represents the union of two pointer sets: every element in the resulting set is either in

*X* and/or in

*Y*, and every element of either

*X* and

*Y* is in the resulting pointer set.

>

**X ∪ Y**
ptrset set_intersection(ptrset X, ptrsetY)

Represents the intersection of two pointer sets: every element in the resulting set is in

*X* and

*Y*, and every element in both

*X* and

*Y* is in the resulting pointer set.

>

**X ∩ Y**
bool set_in(void* x, ptrset Y)

Expresses the fact that a certain pointer

*x* is in the pointer set

*Y*.

>

**x ∈ Y**
bool set_eq(ptrset X, ptrset Y)
bool set_equal(ptrset X, ptrset Y)

Expresses the equality of the two pointer sets by expressing that both sets contain the same elements (i.e. pointer).

>

**∀p: (p ∈ X) ⇔ (p ∈ Y)**
bool set_disjoint(ptrset X, ptrset Y)

Expresses the disjointness of two pointer sets

*X* and

*Y* by expressing that no element (i.e. pointer) is contained in both sets.

>

**X ∩ Y = {}**
bool set_subset(ptrset X, ptrset Y)

Expresses the fact that set

*X* is a subset of set

*Y*: each element (i.e. pointer) of set

*x* is also contained in set

*Y*.

>

**X ⊆ Y**
ptrset set_empty()

Represents the empty pointer set.

>

**{ }**
ptrset set_universe()

Represents the pointer set containing all possible void pointers.

>

**∀ p: p ∈ result**
size_t set_cardinality(ptrset X)

>

**Only partially implemented at this point. Do not use!**
ptrset SET(...)

> Can be used to specify finite sets by simply enumerating their elements; i.e.,

SET()

> is the empty set:

**{ }**
SET(a,b,c)

> is the set

**{a, b, c}**