Techniques for Logic Programming: A Short Survey
The importance of program verification
is nowadays widely recognized also in logic programming. The efforts of many researchers
in this field has led to the introduction of various verification techniques, which vary
according to the program properties one is interested to prove. One can divide these
properties into two main classes. Declarative properties refer to the logical meaning of a
program, that is, a description independent from the underlying computational mechanism.
Run-time properties describe the form of the arguments of an atom at the moment of its
call/success in the program.
This paper presents a short panoramic
of various verification techniques that have been proposed in the literature, in the form
of a brief summary of the main approaches. We review proof methods for declarative
properties and for run-time properties, and refer to recent work on the relationship
between verification techniques and abstract interpretation.
A thorough treatment of verification
techniques for logic programming can be found, for instance, in
[2, 11, 17], as well as in a recent book by Apt , which deals in particular with the
topic of verification of Prolog programs.
2 Verification Techniques
2.1 Proof Methods for Declarative
Early verification techniques for
declarative properties are mainly based on the following reasoning. The properties of
interest are expressed by a theory in a first-order logic. For instance, consider the
well-known append program:
app([x|xs], ys, [x|zs])* app(xs,
app([ ], ys, ys).
We can consider a theory spec
including a description of lists, together with a specification for the predicate app
(k,l,m) holds if whenever k and l are lists then m is also a list
and k.l=m, where · denotes the concatenation operator on lists. A
program P is said to be correct with respect to spec if P is a
consequence of spec (spec ?P). By the soundness and completeness of
SLD-resolution, it follows that all computed instances are logical consequences of spec.
Thus, in order to prove that a computed instance satisfies a specification spec, it
is sufficient to show that spec ?P. For the program append this
amounts to prove that
spec ?app ([ ], ys,
spec ?app ([x|xs],
ys, [x|zs])* app(xs, ys, zs).
This approach is discussed in various
papers (e.g., [6, 7, 16]). Deransart in  presents a thorough study of proof methods
for declarative properties, and generalizes known results in logic programming by
considering specifications in any domain of interpretation (e.g., non-ground extended
Herbrand bases). Moreover, the author introduces two novel proof methods adapted from
attribute grammar to logic programming (see also ).
2.2 Proof Methods for Run-Time
Run-time properties are useful in, for
instance, program specialization and program optimization. Depending on the expressiveness
of the class of properties which can be described, the following methods have been
2.2.1 Methods Based on Monotonic
In  a program specification, here
called call-success specification, consists of a pair of assertions (pre, post)
associated to each predicate of the program: the pre-condition pre (resp.
post-condition post) describes a property of the arguments of the predicate at the
moment of its call (resp. success) in the program, under the assumption that the Prolog
left-to-right selection rule is used. For instance, we can consider for the predicate app
the precondition pre (arg1, arg2, arg3)
stating that arg1 and arg2 are lists, and the
postcondition post (arg1, arg2, arg3)
stating that arg3 is a list and arg1 . arg2=arg3,
where argi denotes the i-th argument of the predicate app.
In order to prove the correctness of
the program wrt a specification, one has to show the validity of a number of implications
which involve these pre- and post-conditions. For the append example one has to
? pre(,ys,ys) * post([ ],ys,ys),
? pre([x|xs], ys, [x|zs]) * (xs, ys, zs), and
? pre([x|xs], ys, [x|zs]) *
post (xs, ys, zs)*
([x|xs], ys, [x|zs]).
This method is rather intuitive and
easy to use. This is also due to the fact that specifications are supposed to be monotonic,
that is, if a program satisfies a specification then all its instances do. This prevents
the use of assertions on the syntactic form of terms, like the assertion var(x)
which holds only if x is instantiated with a variable (see e.g., ). As a
consequence, this method cannot in general be applied to programs containing extra-logical
features, like built-in predicates on terms. Due to its elegance and relative expressive
power, this method has been used in more recent proposals, where it has been employed as a
basis for defining more refined verification techniques (cf. [1, 18]).
Directional types are a special class
of monotonic call-success specifications. It has been shown (cf. ) that the traditional
notion of well-typedness is subsumed by the notion of correct call-success specification
by Bossi and Cocco . A recent approach by Boye and Maluszynski  introduces an
alternative notion of well-typing condition, which can be applied to Prolog programs where
the traditional notion of well-typedness is not applicable. Moreover, they investigate the
use of the annotation method by Deransart  for proving well-typedness.
2.2.2 General Methods
Drabent and Maluszynski  propose a
verification technique where call-success specifications are not supposed to be monotonic.
Moreover, the assertions used involve two kinds of variables, denoting the arguments of
the predicate at the moment of its call and of its success. Due to its generality, this
method is rather involved, for its verification condition relies on the operational
mechanism of substitution. However, it has been shown in  that this method subsumes the
method of Bossi and Cocco.
In  an alternative proof method to
prove run-time properties is proposed which assigns assertions to
program points. Each assertion describes the form of the variables of the clause when the
flow of control reaches that program point. Also here, the Prolog left-to-right selection
rule is used. There is no assumption on the assertions to be used, thus the method is
applicable also to programs containing built-in predicates. In this way, one can express
global run-time properties, which relate the atoms of a query during its execution.
Observe that this is not possible in general in the previously mentioned methods, since
the pre- and post-condition of a predicate refer only to the arguments of that predicate.
A simpler yet less expressive variant
of this method is contained in .
A comparative study of verification
techniques for proving run-time properties is contained in , where various techniques
are arranged into a hierarchy according to their expressive power.
A recent paper by Drabentm 
addresses the problem of comparing the expressive power of the two main approaches for
proving declarative and run-time properties that we have discussed above. In particular,
the author observes that the call-success specifications are strictly stronger than the
declarative specifications, in the sense that if a program is correct wrt a call-success
specification (pre, post) then it is correct wrt the specification pre * post,
but not vice versa. This observation leads the author to conclude that the approach of
Section 2.1 is the 'natural' approach to use for proving declarative properties, which is
strictly stronger than the one based on call-success specifications used, e.g., in [1,
2.4 Abstract Interpretation and
In order to derive properties of logic
programs in an automatic way, various approximation techniques based on abstract
interpretation  have been introduced. The interested reader is referred to, e.g., 
for a survey on abstract interpretation for logic programming. Two recent papers on the
relationship between abstract interpretation and verification techniques provide a good
basis for comparing these two approaches. Gallardo et al. in  illustrate a natural
connection between abstract interpretation and program verification, by providing a
semantics based on pre- and post-conditions which can be used as a proof method as well as
a collecting semantics for abstract interpretation. Moreover, Volpe and Levi in 
investigate how verification techniques can be reconstructed using abstract
 K.R. Apt. From Logic Programming
to Prolog. Prentice Hall International Series in Computer Science, 1997.
 K.R. Apt and E. Marchiori.
Reasoning about prolog programs: From modes through types to assertions. Formal Aspects
of Computing, 6(6A):743--764, 1994.
 K.R. Apt, E. Marchiori, and C.
Palamidessi. A declarative approach for first-order built-in's of Prolog. Applicable
Algebra in Engineering, Communication and Computation, 5(3/4):159--191, 1994.
 A. Bossi and N. Cocco. Verifying
correctness of logic programs. In Proceedings of Tapsoft '89, pages 96--110.
Springer Verlag, 1989.
 J. Boye and J. Maluszynski.
Directional types and the annotation method. J. Logic Programming, 33(3), 1997. To
 K. L. Clark. Predicate logic as a
computational formalism. Technical Report DOC 79/59, ico-- London, 1979.
 K.L. Clark and S. Tarnlund. A
first order theory of data and programs. Information Processing, 77:939--944, 1977.
 L. Colussi and E. Marchiori.
Proving correctness of logic programs using axiomatic semantics. In Proceedings of the
Eight International Conference on Logic Programming, pages 629--644. The MIT Press,
 P. Cousot and R. Cousot. Abstract
interpretation : a unified lattice model for static analysis of programs by construction
or approximation of fixpoints. In Proceedings of the 4th ACM Symposium on Principles of
Programming Languages, pages 238--251, 1977.
 P. Cousot and R. Cousot. Abstract
interpretation and application to logic programs. J. Logic Programming, 13:103--179,
 P. Deransart. Proof methods of
declarative properties of definite programs. Theoretical Computer Science,
 P. Deransart and J. Maluszynski. A
Grammatical View of Logic Programming. The MIT Press, 1993.
 W. Drabent. It is declarative. In
A. Bossi, editor, ILPS post-conference Workshop on Verification, Model Checking and
Abstract Interpretation, Port Jefferson, Long Island N.Y., USA, 1997.
 W. Drabent and J. Maluszynski.
Inductive assertion method for logic programs. Theoretical Computer Science,
 M.M. Gallardo, P. Merino, and J.M.
Troya. Relating abstract interpretation with logic program verification. In A. Bossi,
editor, ILPS post-conference Workshop on Verification, Model Checking and Abstract
Interpretation, Port Jefferson, Long Island N.Y., USA, 1997.
 C. Hogger. Introduction to Logic
Programming. Academic London, 1984.
 D. Pedreschi. Verification of
logic programs. In M. I. Sessa, editor, 1985-1995 Ten Years of Logic Programming in
Italy, pages 211--233. Palladio, 1995.
 D. Pedreschi and S. Ruggeri.
Verification of logic programs. Technical Report TR-97-05, University of Pisa,
Dipartimento di Informatica, 1997.
 P. Volpe and G. Levi. A
reconstruction of verification techniques by abstract interpretation. In A. Bossi, editor,
ILPS post-conference Workshop on Verification, Model Checking and Abstract
Interpretation, Port Jefferson, Long Island N.Y., USA, 1997.
Universita Ca' Foscari di Venezia
via Torino 155
30173 Mestre-Venezia, Italy