[Next] [Up] [Previous] [Contents]
Next: Vectors and vector operators Up: Set expressions Previous: Extension of operators to

Comprehension expressions

A set may be built iteratively using the construction {f(i):i=x..y}, where f(i) is some expression containing the parameter i, and x, y are integer constants. This expands to the set {f(l),...,f(r)}. For example, the expression:

        { i*i : i = 1..5 }
is equivalent to the set:
        {1,4,9,16,25}
The form {f(i) : i = x..y, c(i)} represents the set of all f(i), for i = x..y such that condition c(i) is true. That is,
        {f(i) : i = x..y, c(i)}  =  {c(x) ? f(x), ... ,c(y) ? f(y)}
For example,
        { i : i = 1..5, i mod 2 = 1}  =   {1,3,5}
Or, for example, if y is of type array 1..5 of boolean, then
        { i : i = 1..5, y[i] }
represents the set of all indices i such that element i of array y is true. Note that in this case, if none of the elements of y is true, the result is undefined. This provides a straightforward way to describe a nondeterministic arbiter. In addition, the contruct provides a way to describe a nondeterministic choice among all the number in a given range except a specified number:
        x := {i : i in 1..5, i ~= j};



Ken McMillan
Sat Jun 6 21:41:59 PDT 1998