Go to the first, previous, next, last section, table of contents.
INVAR declarations
The set of invariant states (i.e. the analogous of normal assignments,
as described in section 3.2.3 ASSIGN declarations) can be specified using a
boolean expression under the `INVAR' keyword. The syntax of a
INVAR declaration is:
invar_declaration :: simple_expr
It is an error for the expression to contain the next() operator,
or to yield any value other than 0 or 1. If there is more
than one INVAR declaration, the invariant set is the conjunction of
all of the INVAR declarations.