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}

Last edited Jun 15, 2009 at 2:00 PM by MichalMoskal, version 1

Comments

No comments yet.