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