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

4.2 Adding the Constraint Store

We now introduce the central notion of a constraint store . This is done in a
similar way as in the constraint logic programming systems, though we need to
take into account here the presence of variables and constants.

Denition 3. We call a constraint evaluated if each constant that occurs in

it is replaced by its value and each variable (not unknown) that occurs in it is
replaced by its current value. If some variable that occurs in

C

C is uninitialized,

we say that the evaluation of yields an error . Otherwise we call the resulting

boolean expression the evaluated form of

C

C .

So no variables occur in the evaluated form of a constraint. For technical
reasons we also consider a false constraint , denoted by

? , that can be generated

only by a constraint solver to indicate contradiction.

Denition 4. A constraint store , in short a store , is a set of evaluated forms
of constraints. We say that an unknown is present in the store if it occurs in a
constraint that belongs to the store.
We call a store failed if

is present in it or if the domain of one of the un-
knowns present in it is empty. By a solution to the store we mean an assignment
of values from the current domains to all unknowns present in it.
Further, we say that a constraint is solved if its evaluated form is satised
by all combinations of values from the current domains of its unknowns.

?

For example, in the program fragment

i:=1;
j:=2;
X[i] <= j;
Y[X[i+2]] <> Y[N];

we have two constraints, X[i] <= j and Y[X[i+2]] <> Y[N] .Here X[1] <= 2
is the evaluated form of the rst one, while Y[X[3]] <> Y[8] is the evaluated
form of the second one. If we deleted the assignment i:=1 the evaluations of
both constraints would yield an error.
The notion of a failed store is a computationally tractable approximation of
that of an inconsistent store, i.e., a store that has no solutions. Indeed, a failed
store is inconsistent but an inconsistent store does not have to be failed: just
consider X[1] = X[2], X[1] < X[2] .

4.3 Interaction Between the Program and the Constraint Store

The program interacts with the store in the following two ways:

{ By adding to it the evaluated forms of the encountered constraints. If the
evaluation of such a constraint yields an error, a run-time error arises.