Logical specification and implementation

It has become customary to focus attention on the semantic aspects of specification and implementation, a model theoretic or algebraic viewpoint. We feel, however, that certain concepts are best dealt with at the syntactic level, rather than via a detour through semantics, and that implementation is one of these concepts. We regard logic as the most appropriate medium for talking about specification (whether of abstract data types, programs, databases, specifications — as an interpretation between theories say, rather than something to do with the embedding of models or mapping of algebras. In this paper, we give a syntactic account of implementation and prove the basic results — composability of implementations and how to deal with structured (hierarchical) specifications modularly — for abstract data types.