zbMATH — the first resource for mathematics

A new technique for verifying and correcting logic programs. (English) Zbl 0884.68033
Summary: A significant extension to a model-building method that we have been developing for several years is presented. A quite complete, albeit reasonably short, description of the previous method is given in order to make this article self-contained. The extension enables the handling of Presburger arithmetic and the deducing of inductive consequences from sets of Horn clauses. For a large class of logic programs the extension also permits the deduction of negative facts and the detection of nontermination. It is shown how the extended method can be used in verifying and correcting programs. The proposed method verifies programs w.r.t. formal specifications, but its fundamentals (i.e., model building) make it useful for pointing out errors and for suggesting a way of correcting wrong programs also w.r.t. informal specifications, such as specifications by examples or specifications using implicit knowledge (the latter features are especially useful when dealing with beginners’ programs). Theoretical properties of the extended method (e.g., soundness and refutational completeness) are proven. The greater power of the extensions to logic programming enabled by our method relative to existing methods and with respect to other standard features (like negation as failure) is also proven. Several nontrivial examples illustrate error detection and correction as well as the broadening of inference capabilities that can be obtained in logic programming by using the rules of this method. These detailed examples show evidence of the interest of our approach. Main directions for future research are given.

68N17 Logic programming
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI