On systematic construction of correct logic programs

TL;DR

This paper introduces a systematic, declarative approach for constructing correct and semi-complete logic programs based on formal semantics, aiding programmers in ensuring correctness relative to specifications.

Contribution

It presents a new method for building provably correct logic programs using Kunen's and well-founded semantics, abstracting operational details.

Findings

Method is simple and practical for everyday programming

Applicable to normal programs under specific semantics

Ensures correctness and semi-completeness relative to specifications

Abstract

Partial correctness of imperative or functional programming divides in logic programming into two notions. Correctness means that all answers of the program are compatible with the specification. Completeness means that the program produces all the answers required by the specifications. We also consider semi-completeness -- completeness for those queries for which the program does not diverge. This paper presents an approach to systematically construct provably correct and semi-complete logic programs, for a given specification. Normal programs are considered, under Kunen's 3-valued completion semantics (of negation as finite failure) and the well-founded semantics (of negation as possibly infinite failure). The approach is declarative, it abstracts from details of operational semantics, like e.g.\ the form of the selected literals (``procedure calls'') during the computation. The proposed method is simple, and can be used (maybe informally) in actual everyday programming.