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
Thom Frühwirth presented a short, elegant and efficient Prolog program for the n queens problem. However the program may be seen as rather tricky and one may be not convinced about its correctness. This paper explains the program in a declarative way, and provides proofs of its correctness and completeness. The specification and the proofs are declarative, i.e. they abstract from any operational semantics. The specification is approximate, it is unnecessary to describe the program's semantics exactly. Despite the program works on non-ground terms, this work employs the standard semantics, based on logical consequence and Herbrand interpretations.
Another purpose of the paper is to present an example of precise declarative reasoning about the semantics of a logic program.
Keywords: logic programming, declarative programming, program completeness, program correctness, specification, non-ground answers
Most known results on avoiding the occur-check are based on the notion of "not subject to occur-check" (NSTO). It means that unification is performed only on such pairs of atoms for which the occur-check never succeeds in any run of a nondeterministic unification algorithm. Here we show that this requirement is too strong. We show how to weaken it, and present some related sufficient conditions under which the occur-check may be safely omitted. We show examples for which the proposed approach provides more general results than the approaches based on well-moded and nicely moded programs (this includes cases to which the latter approaches are inapplicable).
Keywords: occur-check, unification, modes, delays
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.See also an example proof and a report on completeness of the method here.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.