We discuss proving correctness and completeness of definite clause logic programs. We propose a method for proving completeness, while for proving correctness we employ a method which should be well known but is often neglected. Also, we show how to prove completeness and correctness in the presence of SLD-tree pruning, and point out that approximate specifications simplify specifications and proofs.
We compare the proof methods to declarative diagnosis (algorithmic debugging), showing that approximate specifications eliminate a major drawback of the latter. We argue that our proof methods reflect natural declarative thinking about programs, and that they can be used, formally or informally, in every-day programming.
Keywords: logic programming, declarative programming, program completeness, program correctness, specifications, declarative diagnosis / algorithmic debugging
This paper presents an example of formal reasoning about the semantics of a Prolog program of practical importance (the SAT solver of Howe and King). The program is treated as a definite clause logic program with added control. The logic program is constructed by means of stepwise refinement, hand in hand with its correctness and completeness proofs. The proofs are declarative -- they do not refer to any operational semantics. Each step of the logic program construction follows a systematic approach to constructing programs which are provably correct and complete. We also prove that correctness and completeness of the logic program is preserved in the final Prolog program. Additionally, we prove termination, occur-check freedom and non-floundering.
Our example shows how dealing with ``logic'' and with ``control'' can be separated. Most of the proofs can be done at the ``logic'' level, abstracting from any operational semantics.
The example employs approximate specifications; they are crucial in simplifying reasoning about logic programs. It also shows that the paradigm of semantics-preserving program transformations may be not sufficient. We suggest considering transformations which preserve correctness and completeness with respect to an approximate specification.
Keywords: logic programming, declarative programming, program completeness, program correctness, specification, program transformation, floundering, occur-check
A sufficient and necessary condition is given under which least Herbrand models exactly characterize the answers of definite clause programs.
Keywords: logic programming, least Herbrand model, declarative semantics, function symbols
Completeness of a logic program means that the program produces all the answers required by its specification. The cut is an important construct of programming language Prolog. It prunes part of the search space, this may result in a loss of completeness. This paper proposes a way of proving completeness of programs with the cut. The semantics of the cut is formalized by describing how SLD-trees are pruned. A sufficient condition for completeness is presented, proved sound, and illustrated by examples.
Keywords: logic programming, the cut, operational semantics, program completeness, program correctness
The paper presents a simple and concise proof of correctness of the magic transformation. We believe it may provide a useful example of formal reasoning about logic programs.
The correctness property concerns the declarative semantics. The proof, however, refers to the operational semantics (LD-resolution) of the source programs. Its conciseness is due to applying a suitable proof method.
Keywords: program correctness, logic programming, magic transformation, declarative semantics, LD-resolution, operational semantics
We present an inductive assertion method for proving run-time properties of logic programs. The method could be seen as a logic programming counterpart of the well-known approach of Floyd and Hoare for imperative programs. The method concerns assertions assigned to program points and makes it possible to prove that whenever the control reaches a program point the corresponding assertion is satisfied. We also show a way of augmenting the method to prove termination. An assertion (assigned to a point in a program clause) describes a set of substitutions (for the variables of the clause). Assertions may be not monotonic (i.e. not closed under substitutions).
Certain properties of logic programs are inexpressible in terms of their declarative semantics. One example of such properties would be the actual form of procedure calls and successes which occur during computations of a program. They are often used by programmers in their informal reasoning.
In this paper, the inductive assertion method for proving partial correctness of logic programs is introduced and proved sound. The method makes it possible to formulate and prove properties which are inexpressible in terms of the declarative semantics. An execution mechanism using the Prolog computation rule and arbitrary search strategy (eg. OR-parallelism or Prolog backtracking) is assumed. The method may be also used to specify the semantics of some extra-logical built-in procedures for which the declarative semantics is not applicable.