The Alma Project, or How First-Order Logic Can Help Us in Imperative Programming - Correct System Design: Recent Insights and Advances - page 95

co: Colour;
No: CONSTRAINED INTEGER;
END;
VAR i, j: INTEGER;
a: ARRAY [1..N] of INTEGER;
C: CONSTRAINED [1..N];
X, Y: Board;
Z: Info;

So a , i and j are variables while C is an unknown. In turn, X and Y are arrays
of unknowns and Z is a record the rst component of which is a variable and the
second an unknown.
Because of the syntax of , boolean expressions can appear both in the

position of a statement and inside a condition.

Alma-0

Denition 2. A constraint is a boolean expression that involves some unknowns.
We postulate that the unknowns can appear only within constraints or within
the right hand side of an assignment.

The values of unknowns are determined only by means of constraints that
are placed on them. In particular, by the just introduced syntactic restriction,
one cannot use assignment to assign a value to an unknown. So in presence
of the above declarations the statements X[1] := 0 and C:=1 are illegal. In
contrast, the constraints X[1] = 0 and C=1 are legal. Further, the assignments
i := X[1] + X[2] and i := Y[X[2]] are also legal statements.
Initially each unknown has an undetermined value that belongs to the domain
associated with the type. By placing constraints on an unknown its domain can
shrink . The unknown continues to have an undetermined value until the domain
gets reduced to a singleton.
If the program control reaches an occurrence of an unknown outside of a
constraint, so within the right hand side of an assignment, this unknown is
evaluated. If its value is at this moment undetermined, this evaluation yields a
run-time error. If the value is determined (that is, the domain is a singleton),
then it is substituted for the occurrence of the unknown. So the occurrences of
an unknown outside of a constraint are treated as usual variables.
Note that during the program execution the domain of an unknown mono-
tonically decreases with respect to the subset ordering. This is in stark contrast
with the case of variables. Initially, the value of a variable of a simple type is
not known but after the rst assignment to it its value is determined though can
non-monotonically change to any other value from its type.
Intuitively, a program is viewed as an \engine" that generates constraints.
These constraints are gradually solved by means of the constraint solving process
that we shall explain now.