Most of the operators extend to sets, in a way which is consistent with the interpretation of sets as independent nondeterministic choices. Generally, a unary operator f obeys the law
f{x,y} = {f(x),f(y)}Thus, for example,
-(2..3) = (-2..-3)and
~{0,1} = {1,0}For a binary operator *, we have
{x,y} * z = {x * z, y * z} x * {y,z} = {x * y, x * z}For example,
3 + {4,5} = {7,8}and
0 & {0,1} = 0 1 & {0,1} = {0,1}(which are actually special cases of the laws given above for ``and'').
This behavior of sets is somewhat counterintuitive when the equality operator is applied to sets. For example, the result of
{a,b} = {a,b}is not equal to 1 (true). The way to understand this is to think of each set as representing an arbitrary choice among its elements. Thus, the result of the above expression is the set
The exception to the above rule is the ``in'' operator, which compares a value and a set of values. In this case, only the left represents a nondeterministic choice. That is:
{x,y} in z = {x in z, y in z}However, as stated previously,
x in {y,z} = (x in y) | (x in z)
[N.B. This makes ``in'' the only operator in the language which is not monotonic with respect to set containment. The ``in'' operator is only monotonic in its left argument. A formal verification system that relies on monotonicity (such as ternary symbolic simulation) should allow only constant sets on the right hand side of ``in''.]