next up previous
Next: 3.2 Presburger formula operations Up: 3 Relational Expression syntax Previous: 3 Relational Expression syntax

3.1 Relations

A relation is an operand of a relational expression. Its syntax is:

{ [ InputList ] -> [ OutputList ] : formula }

InputList and OutputList are lists of tuple elements. A tuple element can be:

The formula is optional. If it is omitted, no constraints other than those introduced by the input and output expressions are imposed upon the relation's variables. Otherwise, the formula describes additional constraints on variables used in the relation.

3.1.1 Sets

In addition to relations, the system can represent sets.

When a relation is declared with only one tuple, as in:

{ [ SetList ] : formula }
then the relation becomes a set. The variables that are used to describe a set ( SetList) are called set variables rather than input or output variables.