120
Chapter
4.
Programs
§19. Declarative Error Diagnosis
121
[73], [74]). Improved fonns
of
negation are being introduced (e.g., [75], [104]).
There has been work on program transfonnation, which allows programmers to
write programs in a
fonn
closer to their specification (e.g., [101] and the references
therein).
The advanced logic programming systems, which will become available in the
near future, will be compiler systems exploiting all the above techniques. Source
programs for these systems will be written in a subset
of
fIrst order logic. This
subset will include at least the class
of
programs defIned in this chapter.
In
the
first stage
of
compilation, source programs will be transformed into assembly
programs by the automatic addition
of
control infonnation and the application
of
various transformation techniques. These assembly language programs will be
similar to PROLOG programs as they are currently written for a coroutining
system. In the second·stage
of
compilation, the assembly program will be further
compiled into a machine program, which can then be run on a coroutining version
of
Warren's abstract PROLOG machine [110]. This second compilation stage is
now well understood. Note that, according to the above view, current versions
of
PROLOG, which are now regarded as high level languages, will eventually be
regarded as low level machine languages.
Such systems will allow programmers to write in a more declarative style than
is currently possible and should ensure a great decrease in programmer effort.
However, there is a catch. The compiled program could be so different from the
source program and the control could be so complicated that debugging such
programs by conventional tracing techniques is likely to be extraordinarily diffIcult.
In
other words, the programmer may only require an understanding
of
the intended
interpretation to write the program, but will need to know everything about the
computational behaviour
of
the system to debug the program! In fact, this problem
in a less extreme form also plagues current PROLOG systems.
For this reason, we argue that an indispensable component
of
future logic
programming systems will be a declarative debugging system, that is, one that can
be used without the need to understand the computational behaviour
of
the system.
The main purpose
of
this section
is
to present a declarative error diagnoser which
fInds errors in programs that use advanced control facilities and the increased
expressiveness
of
program statements. Attention
is
confIned to errors which lead
to a wrong
or
missing solution. In particular, errors which lead to infInite loops
are not discussed here.
Declarative error diagnosis was introduced into logic programming, under the
name algorithmic debugging, by Shapiro [92]. As well as an error diagnoser, he
also presented an error corrector (regarded as a kind
of
inductive program
synthesiser). Shapiro was mainly concerned with defInite programs using
~e
standard computation rule. Av-Ron
[6]
studied top-down diagnosers for defImte
programs. Under the name rational debugging, Pereira [81] presented a diagnoser
for arbitrary PROLOG programs, including the non-declarative features
of
PROLOG, such as cut. More recently, Ferrand [34] gave a mathematical analysis
of
an error diagnoser for defInite programs. Other work on debugging (not
necessarily declarative) is contained in [12], [30], [31], [32], [83] and the
references therein.
We
now give the defInitions
of
the concepts necessary for a foundation for
error diagnosis.
Definition Let P be a program. An intended interpretation for P is a nonnal
Herbrand interpretation for comp(P).
The restriction to Herbrand interpretations is not essential. However, in
practice, intended interpretations are usually Herbrand and the analysis is a
li~tle
easier in this case. The foremost aim
of
a programmer is to write programs
WhICh
have their intended interpretations as models. This leads to the following
defInition.
Definition Let P
be
a program and I an intended interpretation for P.
We
say P
is correct wrt I
if
I is a model for comp(p); otherwise, we say that P
is
incorrect
wrtI.
Of
course, the reason we want P to be correct wrt I is so that all answers
computed
by
P will be true wrt I.
Proposition 19.1 Let P be a program, G a goal
~W,
and e a
comput~d
answer for P u {G}. Let I be an intended interpretation for P and suppose that P
IS
correct wrt I. Then
we
is valid in I.
Proof The result follows immediately from the soundness
of
SLDNF-resolution
(theorem 18.7), since I is a model for comp(P). iii
However, even
if
P
is
correct wrt I, we cannot guarantee that P will compute
everything
in
I.