Previous: AIDA-96-03 Next: AIDA-96-05 Index 1996


Intellectics Group: Technical Report 96-04

The Relation between Logic Programs and Specification

Kung-Kiu Lau and Mario Ornaghi

The fundamental relation between a program P and its specification S is correctness: P satisfies S if and only if P is correct wrt S. In logic programming, this relationship can be particularly close, since logic can be used to express both specifications and progams. Indeed logic programs are often regarded and used as (executable) specifications themselves. In this paper, we argue that the relation between S and P should be firmly set in the context of the underlying problem domain, which we call a framework F, and we give a model-theoretic view of the correctness relation between specifications and programs in F. We show that the correctness relation between S and P is always well-defined. It thus provides a basis for properly distinguishing between S and P. We use the subset example throughout, to illustrate our model-theoretic approach.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry