The Relationship Between Logic Programs And Specifications --- The Subset Example Revisited Kung-Kiu Lau Department of Computer Science, University of Manchester Oxford Road, Manchester M13 9PL, United Kingdom kung-kiu@cs.man.ac.uk Mario Ornaghi Dipartimento di Scienze dell'Informazione Universita' degli studi di Milano Via Comelico 39/41, Milano, Italy ornaghi@dsi.unimi.it Abstract: 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 programs. 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.