Expressions with Bound Variables

Operations on collections

Several operations are provided on values of the built-in collection types set, bag and seq. In each case you need to declare a bound variable, which has the type of a single element of the collection.

In the following, condition and expression are expressions that involve the bound variable identifier.

  forall identifier::collection :- condition

yields true if all the elements of collection satisfy condition, or if collection is empty.
For example,

  forall c::"4321" :- c.isDigit

yields true. (The literal "4321" has type seq of char - also called string).

An expression of the form

  exists identifier::collection :- condition

yields true if at least one of the elements of collection satisfies condition. So

  exists c::"hello world" :- c.isDigit

yields false.

The expression

  those identifier::collection :- condition

yields a result of the same type as collection comprising those elements of collection that satisfy condition.
For example,

  those q::"hello world" :- q ~in "aeiou"

yields "hll wrld".

An expression of the form

  that identifier::collection :- condition

yields the element of collection that satisfies condition (there must be exactly one). So

  that x::seq of int{1, 10, 100} :- 5 < x < 50

is well-formed and has the value 10.

The expression

  any identifier::collection :- condition

yields any element of collection that satisfies condition (there must be at least one). For example, any w::1..10 :- w%2 = 0 could yield any of 2, 4, 6, 8 or 10. (Recall that 1..10 constructs a sequence of the integers 1 to 10 in ascending order, and % is the remainder or modulo operator).

The last expression type in this group is a little more complicated but very powerful. The expression

  for identifier::collection yield expression

yields a result similar to collection except the element type is the type of expression. The result comprises the elements in collection mapped to the values defined by expression. For example,

  for x::"ibm" yield <x

yields "hal" (in this case, expression has the same type as the elements of collection, so the result type is the same as the type of collection).

An expression of the form

  for those identifier::collection :- condition yield expression

is similar, but only those elements of collection that satisfy condition are taken. So if you can remember what conditional expressions look like, you should be able to satisfy yourself that

  for those thingy::"Go 4 it!"
     :- thingy.isLetter | thingy.isDigit
     yield ([thingy.isLetter]: "letter", []: "digit")

is equal to

  seq of string{"letter", "letter", "digit", "letter", "letter"}.

If you use any of these expressions as an operand in a larger expression, you will need to enclose it in brackets.

Variations on expressions involving bound variables

Some of the expressions introduced in the preceding section have alternative forms.

First, in the forall and exists expressions, you can declare the bound variable as having a type instead of belonging to a collection. The bound variable then ranges over all possible values of that type. The type may be finite (e.g. an enumeration type), or infinite (e.g. int).

Now, it may seem odd that in a forall or exists expression, the bound variable is allowed to range over an infinite type. Surely such an expression could take an infinite amount of time to compute? This is true, which is why Perfect Developer will refuse to generate code if the type is infinite. However, it can be useful to use these sorts of expressions in specifications, and the validator is used to handling them.

You can also declare more than one bound variable in a forall or exists expression (see the Language Reference Manual for details).

Second, in the that expression, you can abbreviate that identifier::collection :- true to that collection. Obviously, collection had better contain exactly one element! You can do the same for the any expression.

Next:  Sequences