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 construct
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};