Next: Innovative aspects Up: Description of the Previous: Current state-of-the-art

## Detailed description of the research work

The overall objective of the research work is to study the foundational aspects of the problem of program verification with the purpose of constructing a theory of verification which serves as a rigorous basis for the design of an automatic program verifier. The practical outcome of this preliminary formal activity should be the realization of a prototype verifier for logic programs, whose relevance for solving ``real-life'' problems should be tested on a wide range of examples. The automation of reasoning about computer programs is one of the main objectives in the field of program verification. To this aim, mechanical theorem-proving is crucial. As a result, formal proofs seem to be attractive, and, indeed, there are now a number of techniques for obtaining in a formal system an expression whose formal proof or disproof constitutes a verification that a given program has a given property. The tendency is, roughly, to represent properties of programs as theorems in the first-order predicate calculus; in this form established mechanical theorem proving techniques might be relevant to automating the verification process. By restricting the attention on logic programs, we dispose of a very specialized theorem-prover which is SLD-resolution. The idea is, then, to use resolution-based techniques (e.g. some extensions of the SLD-resolution) for proving properties of logic programs. The main problem in doing so is that the resolution theorem-proving tradition does not handle axiom schemes, such as mathematical induction. And, as argued by almost all authors in the field, induction in one form or another is unavoidable in proving properties of programs. This is because the objects about which computer programmers think (integers, sequences, trees, lists etc.) are usually inductively defined concepts. Moreover, a program can be seen as a finite description of a usually infinite class of arbitrarily long computation sequences: induction is a finite process by which the infinite can be defined. Therefore, it seems necessary to find out a way to incorporate the power of induction in a resolution-based framework and use query evaluation for the proofs of logic program properties. There are two possibilities: one of them tries to get the effect of induction by means of some loop detection tools; the other one faces the problem directly by using a higher order logic language in which simply typed -terms can express the inductive nature of a specification formula.

The first approach is based on the view of program properties as integrity constraints, and has been previously investigated by Kowalski ([22]) and Lever ([23]). In Logic Programming, integrity constraints are often written as queries that can be evaluated by SLDNF-resolution, [8,24] (or some variants of it). One of the problems with this approach is that, as most properties of interest involve recursively defined predicates, evaluation of properties expressed as queries commonly generates infinite trees. Since the existence of an infinite failed SLDNF-resolution for a property is not in itself sufficient to determine that the property is a consequence of the completion of the program, soundness results are not easy to achieve. In [23] the use of SLS-resolution instead of SLDNF-resolution eliminates these difficulties. Another problem with the use of SLDNF-resolution is that negation by failure doesn't correctly treat variables. We propose to avoid this problem by using an extension of the Negation As Failure rule, which is able to deal with existentially quantified negative queries, namely the Negation As Instantiation rule (NAI, [15]). By augmenting NAI by loop detection we could avoid the problem with the infinite branches, which still remains in the interpreter extended by the NAI rule. Since the interpreter of LP palys a fundamental role in this approach, we believe that this can be generalized to other logic programming languages, such as constraint logic programming [20], and concurrent constraint programming [27,28], by considering the interpreters for those languages instead of Prolog.

As for the second approach, the starting point of the research is the observation that induction axiom schemata are in effect really just single second-order formulas

with the second-order quantifier dropped:

so that one can substitute any predicate , where S is any first order sentence with one free variable k, for P and get an axiom. Thus, a higher-order logic programming language like -Prolog ([26,25]) could be used to implement such theorem proving systems. However, building a prover could be very complicated. An alternative could be to use already existing systems, such as the Isabelle theorem prover ([17,18]), which is built on higher-order resolution, augmented with theories for doing induction. The Coq system could also be a good candidate, since it has higher-order quantification and induction even though it has not resolution.

Next: Innovative aspects Up: Description of the Previous: Current state-of-the-art

David Gilbert
Thu Jun 20 09:47:49 BST 1996