Elena Marchiori

1 Introduction

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 [1], which deals in particular with the topic of verification of Prolog programs.

2 Verification Techniques

2.1 Proof Methods for Declarative Properties

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, ys, zs)

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 logical 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, ys), and

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 [11] 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 [12]).

2.2 Proof Methods for Run-Time Properties

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 introduced.

2.2.1 Methods Based on Monotonic Assertions

In [4] 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 (arg₁, arg₂, arg₃) stating that arg₁ and arg₂ are lists, and the postcondition post (arg₁, arg₂, arg₃) stating that arg₃ is a list and arg₁ . arg₂=arg₃, where arg_i 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 prove that

? 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., [3]). 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. [2]) that the traditional notion of well-typedness is subsumed by the notion of correct call-success specification by Bossi and Cocco [4]. A recent approach by Boye and Maluszynski [5] 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 [11] for proving well-typedness.

2.2.2 General Methods

Drabent and Maluszynski [14] 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 [2] that this method subsumes the method of Bossi and Cocco.

In [8] 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 [2].

2.3 Comparison

A comparative study of verification techniques for proving run-time properties is contained in [2], where various techniques are arranged into a hierarchy according to their expressive power.

A recent paper by Drabentm [13] 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, 18].

2.4 Abstract Interpretation and Verification Techniques

In order to derive properties of logic programs in an automatic way, various approximation techniques based on abstract interpretation [9] have been introduced. The interested reader is referred to, e.g., [10] 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 [15] 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 [19] investigate how verification techniques can be reconstructed using abstract interpretation.

References

[1] K.R. Apt. From Logic Programming to Prolog. Prentice Hall International Series in Computer Science, 1997.

[2] 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.

[3] 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.

[4] A. Bossi and N. Cocco. Verifying correctness of logic programs. In Proceedings of Tapsoft '89, pages 96--110. Springer Verlag, 1989.

[5] J. Boye and J. Maluszynski. Directional types and the annotation method. J. Logic Programming, 33(3), 1997. To appear.

[6] K. L. Clark. Predicate logic as a computational formalism. Technical Report DOC 79/59, ico-- London, 1979.

[7] K.L. Clark and S. Tarnlund. A first order theory of data and programs. Information Processing, 77:939--944, 1977.

[8] 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, 1991.

[9] 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.

[10] P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. J. Logic Programming, 13:103--179, 1992.

[11] P. Deransart. Proof methods of declarative properties of definite programs. Theoretical Computer Science, 118:99--166, 1993.

[12] P. Deransart and J. Maluszynski. A Grammatical View of Logic Programming. The MIT Press, 1993.

[13] 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.

[14] W. Drabent and J. Maluszynski. Inductive assertion method for logic programs. Theoretical Computer Science, 59(1):133--155, 1988.

[15] 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.

[16] C. Hogger. Introduction to Logic Programming. Academic London, 1984.

[17] 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.

[18] D. Pedreschi and S. Ruggeri. Verification of logic programs. Technical Report TR-97-05, University of Pisa, Dipartimento di Informatica, 1997.

[19] 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.

Elena Marchiori

Universita Ca' Foscari di Venezia

via Torino 155

30173 Mestre-Venezia, Italy