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

6 Language Extensions

In this section we discuss some built-in procedures of the proposed language
that make it easier for the user to program with constraints. In particular, in
Subsection 6.1 we discuss built-ins for stating constraints, and in Subsection 6.2
we present built-ins for assigning values to unknowns.

6.1 Built-ins for Expressing Constraints

The practice of constraint programming requires inclusion in the programming
language of a certain number of language built-ins that facilitate constraint
formulation.
For example, if we wish to state that the unknowns of the array X must have
pairwise dierent values, we write

ALL_DIFFERENT(X);

This call results in a constraint which is equivalent to the set of all the
corresponding constraints of the form X[i] <> X[j] ,for i 2

[1..N-1] and j

[i+1..N] . 1
Similarly, if we wish to state that at most k among the unknowns belonging
to the array X can have the value v ,wewrite

2

AT_MOST(k,X,v);

This sort of built-ins on arrays are present in other imperative constraint
languages. We do not list all of them here, but we envision their presence in the
language.
Such built-ins on arrays are the counterparts in imperative languages of the
corresponding built-ins on lists provided by constraint logic programming sys-
tems such as CHIP. These languages also support symbolic manipulation of
terms which makes it easy to generate arithmetic constraints. The traditional
imperative programming languages lack this power and exclusive reliance on
arrays can lead to articial and inecient solutions.
For example, suppose we are given an

of integer unknowns
and we wish to state the constraint that the sum of the elements of the main
diagonal must be equal to a given value

n n matrix A

. A customary solution would involve
resorting to an auxiliary array of unknowns in the following way:

b

VAR A: ARRAY [1..N], [1..N] OF CONSTRAINED INTEGER;
V: ARRAY [1..N] OF CONSTRAINED INTEGER;
b: INTEGER;

V[1] = A[1,1];
1 In some systems, such a constraint is kept in its original form in order to exploit
constraint propagation techniques that deal specically with constraints of this kind,
see [17].