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

We assume here that the constraint solver that deals with linear equations
over reals is suciently powerful to solve the generated equations.
Finally, we present a solution to the Frequency Assignment problem (Prob-
lem 1) that uses constraints. Again, we only write the part of the program that
generates constraints. We assume here that the variables S and F are properly
initialized.

TYPE SeparationMatrix = ARRAY [1..N],[1..N] OF INTEGER;
IllegalFrequencies = ARRAY [1..N],[1..M] OF BOOLEAN;
Assignment = ARRAY [1..N] OF CONSTRAINED [1..M];
VAR S: SeparationMatrix;
F: IllegalFrequencies;
X: Assignment;
i, j: INTEGER;

BEGIN
FORi:=1TONDO
FORj:=1TOMDO
IF F[i,j] THEN X[i] <> j END
END
END;
FORi:=1TONDO
FOR j := 1 TO i-1 DO
EITHER X[i] - X[j] >= S[i,j]
ORELSE X[j] - X[i] >= S[i,j]
END
END
END
END;

The use of the ORELSE statement creates here choice points to which the
control can return if in the part of the program that deals with constraints
solving a failed store is produced.
Alternatively, one could use here a disjunction and replace the ORELSE state-
ment by

(X[i] - X[j] >= S[j,i]) OR (X[j] - X[i] >= S[j,i]) .

In this case no choice points are created but the problem of solving (disjunctive)
constraints is now \relegated" to the store.
The latter solution is preferred if the constraint solver in use is able to perform
some form of preprocessing on disjunctive constraints, such as the constructive
disjunction of [8]. On the other hand, the former solution allows the programmer
to retain control upon the choice generated by the system. For example, she/he
can associate dierent actions to the two branches of the ORELSE statement.
It is important to realize that the integration of constraints to as

outlined in this section is possible only because the unknowns are initially unini-
tialized.

Alma-0