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

gramming languages depend in essential way on some features as the presence
of constraint solvers (for example a package for linear programming) and con-
straint propagation. So this extension of logic programming goes beyond rst-
order logic.
It is also useful to reflect on other limitations of these two formalisms. Both
logic programming and constraint logic programming languages rely heavily on
recursion and the more elementary and easier to understand concept of iteration
is not available as a primitive. Further, types are absent. They can be added to
the logic programming paradigm and in fact a number of successful proposals
have been made, see, e.g., [15]. But to our knowledge no successful proposal
dealing with addition of types to constraint logic programs is available.
Another, admittedly debatable, issue is assignment, shunned in logic pro-
gramming and constraint logic programming because its use destroys the declara-
tive interpretation of a program as a formula. However, we nd that assignment
is a useful construct. Some uses of it, such as recording the initial value of a
variable or counting the number of bounded iterations, can be replaced by con-
ceptually simpler constructs but some other uses of it such as for counting or for
recording purposes are much less natural when simulated using logic formulas.

1.2 Design Decisions

These considerations have led us to a design of a programming language .

The initial work on the design of this language was reported in [3]; the nal
description of the language, its implementation and semantics is presented in
[2].

Alma-0

In a nutshell, Alma-0 has the following characteristics:

{ it is an extension of a subset of Modula-2 that includes assignment, so it is
a strongly typed imperative language;
{ to record the initial value of a variable the equality can be used;
{ it supports so-called \don't know" nondeterminism by providing a possibility
of a creation of choice points and automatic backtracking;
{ it provides two forms of bounded iterations.

The last two features allow us to dispense with many uses of recursion that
are in our opinion dicult to understand and to reason about.
As we shall see, the resulting language proposal makes programming in an
imperative style easier and it facilitates (possibly automated) program veri-
cation. Additionally, for several algorithmic problems the solutions oered by
Alma-0 is substantially simpler than the one oered by the logic programming

paradigm.
The following simple example can help to understand what we mean by
saying that

programs
are simpler than their imperative and logic programming counterparts.
Consider the procedure that tests whether an array a[1..n] is ordered. The
customary way to write it in Modula-2 is:

Alma-0 is based on rst-order logic and that some Alma-0