Implementation Specifications

Abstract

Loose specifications of abstract data types (ADTs) have many non-isomorphic algebras as models. An implementation between two loose specifications should therefore consider many abstraction functions together with their source and target algebras. Just like specifications are stepwise refined to restrict their class of models, implementations should be stepwise refinable to restrict the class of abstraction functions. In this scenario specifications and implementations can be developed interwovenly. For example, we can consider implementations of sets by lists where the set simulating list operations are still left open. They may be refined later on so that an implementation of sets by arbitrary lists, by lists without double entries, or by sorted lists is obtained, differing e.g. in the efficiency of the set simulating operations. We suggest to have implementation specifications analogously to loose ADT specifications: Implementations have signatures, models, axioms and sentences thus constituting an institution. Implementation specifications are the theories of this institution and refinements between implementation specifications are its theory morphisms.