Stepwise refinement of algebraic specifications is a well known formal method- ology for program development. However, traditional notions of refinement based on signa- ture morphisms are often too rigid to capture a number of relevant transformations in the context of software design, reuse, and adaptation. This paper proposes a new approach to refinement in which signature morphisms are replaced by logical interpretations as a means to witness refinements. The approach is first presented in the context of equational logic, and later generalised to deductive systems of arbitrary dimension. This allows, for example, refining sentential into equational specifications and the latter into modal ones.
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. This paper outlines a logical approach to abstract data types, which is motivated by, and more adequate for (than algebraic approaches), the practice of programming. Abstract data types are specified as axiomatic theories and notions concerning the former are captured by syntactical concepts concerning the latter. The basic concepts of nambility, conservative extensions and interpretations of theories explain implementation, refinement and parameterisation. Being simple, natural and flexible, this approach is quite appropriate for program development.