liu.seSearch for publications in DiVA
Change search
ReferencesLink to record
Permanent link

Direct link
Proving correctness and completeness of normal programs - A declarative approach
Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, TCSLAB - Theoretical Computer Science Laboratory.
Milkowska, M., Institute of Informatics, Warsaw University, ul. Banacha 2, 02-097 Warszawa, Poland.
2005 (English)In: Theory and Practice of Logic Programming, ISSN 1471-0684, Vol. 5, no 6, 669-711 p.Article, review/survey (Refereed) Published
Abstract [en]

We advocate a declarative approach to proving properties of logic programs. Total correctness can be separated into correctness, completeness and clean termination, the latter includes non-floundering. Only clean termination depends on the operational semantics, in particular on the selection rule. We show how to deal with correctness and completeness in a declarative way, treating programs only from the logical point of view. Specifications used in this approach are interpretations (or theories). We point out that specifications for correctness may differ from those for completeness, as usually there are answers which are neither considered erroneous nor required to be computed. We present proof methods for correctness and completeness for definite programs and generalize them to normal programs. For normal programs we use the 3-valued completion semantics, this is a standard semantics corresponding to negation as finite failure. The proof methods employ solely the classical 2-valued logic. We use a 2-valued characterization of the 3-valued completion semantics, which may be of separate interest. The method of proving correctness of definite programs is not new and can be traced back to the work of clark in 1979. However a more complicated approach using operational semantics was proposed by some authors. We show that it is not stronger than the declarative one, as far as properties of program answers are concerned. For a corresponding operational approach to normal programs, we show that it is (strictly) weaker than our method. We also employ the ideas of this work to generalize a known method of proving termination of normal programs. © 2005 Cambridge Univeristy Press.

Place, publisher, year, edition, pages
2005. Vol. 5, no 6, 669-711 p.
Keyword [en]
Declarative programming, Negation in logic programming, Program correctness and completeness, Specifications, Teaching logic programming, Termination
National Category
Engineering and Technology
URN: urn:nbn:se:liu:diva-50388DOI: 10.1017/S147106840500253XOAI: diva2:271284
Available from: 2009-10-11 Created: 2009-10-11 Last updated: 2011-01-12

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Drabent, Wlodzimierz
By organisation
The Institute of TechnologyTCSLAB - Theoretical Computer Science Laboratory
In the same journal
Theory and Practice of Logic Programming
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 31 hits
ReferencesLink to record
Permanent link

Direct link