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

FORi:=1TONDO
IF R[i] THEN Insert(L,X[i]) END
END;
AT_MOST(max,L,k)
END
END RegionConstraint;

6.2 Built-ins for Assigning Values

In order to search for a solution of a set of constraints, values must be assigned to
unknowns. We dene the built-in procedure INDOMAIN which gets an unknown of
a nite type (so BOOLEAN , enumeration or a subrange type) as a parameter, and
assigns to it one among the elements of its domain. The procedure also creates
a choice point and all other elements of the domain are successively assigned to
the unknown upon backtracking.
The choice of the value to assign to the unknown is taken by the system
depending on the current state of the store, based on predened value selection
strategies. We do not discuss the issue of which are the best value selection
strategies. We only assume that all consistent values are eventually generated,
and that the choice point is erased after the last value has been generated.
The procedure INDOMAIN can be also used on arrays and on lists. For example,
the call INDOMAIN(A) ,where A is a matrix of integer unknowns, generates (upon
backtracking) all possible assignments for all elements of A .
The order of instantiation of the elements of A is taken care of by the store,
which applies built-in strategies to optimize the retrieval of the rst instantiation
of the unknowns. As in the case of value selection, we do not discuss here the
issue of the variable ordering .

7 Related Work

We concentrate here on the related work involving addition of constraints to
imperative languages. For an overview of related work pertaining to the Alma-0

language we refer the reader to [2].
As already mentioned in the introduction, the most successful imperative
constraint language is the C++ library ILOG Solver [9]. The main dierence
between our proposal and ILOG Solver is that the latter is based on the conven-
tional imperative language C++ and consequently it does not support automatic
backtracking. Therefore the interaction with the store cannot be based on fail-
ures issued by the store constraint solvers while evaluating the statements. In
ILOG Solver such an interaction is always explicit, whereas in our proposal we
aim at making it transparent to the user.
We are aware of two other language proposals in which constraints are in-
tegrated into an imperative language | the commercial language CHARME of
[14] and 2LP of [13]. In each language some of the issues here discussed have
been addressed, but not all of them.