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

{ By generating possible values for unknowns that are present in the store by
means of some built-in primitives to be introduced in Subsection 6.2.

The store is equipped with a number of procedures called constraint solvers .
Their form depends on the applications. One or more of them can become ac-
tivated upon addition of (an evaluated form of) a constraint to the store. An
activation of constraint solvers, in the sequel called constraint solving , can re-
duce the domains of the unknowns, determine the values of some unknowns by
reducing the corresponding domains to singletons, delete some constraints that
are solved, or discover that the store is failed, either by generating the false
constraint

or by reducing the domain of an unknown to the empty set.
We assume that constraint solving is a further unspecied process that de-
pending of application may be some form of constraint propagation or a decision
procedure. We require that the result of constraint solving maintains equivalence,
which means that the set of all solutions to the store does not change by applying
to it constraint solvers.
The store interacts with the program as follows.

?

Denition 5. Upon addition of a constraint to the store, constraint solving
takes place.

{ If as a result of the constraint solving the store remains non-failed, the control
returns to the program and the execution proceeds in the usual way.
{ Otherwise the store becomes failed and a failure arises. This means that
the control returns to the last choice point created in the program. Upon
backtracking all the constraints added after the last choice point are retracted
and the values of the variables and the domains of the unknowns are restored
to their values at the moment that the last choice point was created.

This means that we extend the notion of failure, originally introduced in
Section 2, to deal with the presence of the store.
Note that constraints are interpreted in the same way independently of the
fact whether they appear as a statement or inside a condition. For example, the
following program fragment

IF X[1] > 0 THEN S ELSE T END

is executed as follows: The constraint X[1] > 0 is added to the store. If the
store does not fail S is executed, otherwise T is executed. So we do not check
whether X[1] > 0 is entailed by the store and execute S or T accordingly, as
one might intuitively expect. This means that constraints are always interpreted
as so-called tell operations in the store, and never as so-called ask operations,
which check for entailment (see Section 8 for a discussion on this point).

4.4 Examples

To illustrate use of the introduced concepts we now consider three examples. We
begin with the following classical problem.