On implementations of loose abstract data type specifications and their vertical composition

Abstract

In an approach for the implementation of loose abstract data type specifications that completely distinguishes between the syntactical level of specifications and the semantical level of models, vertical implementation composition is defined compatibly on both levels. Implementations have signatures, models, and sentences where the latter also include hidden components, which allows for useful normal form results. We illustrate the stepwise development of implementations as well as their composition by some examples and describe the incorporation of the concept into an integrated software development and verification system.