Direct Implementation of Algebraic Specification of Abstract Data Types

Algebraic specification is now an established way of formally defining abstract data types. For its practical use, however, a segment of program which conforms with the specification has to be generated. Such program segments can be manually produced and must then be verified. Code generation can also be automated, as achieved by the "direct implementation" in [8] where any data type is treated as if its functions produce, manipulate, and access tree structures. We extend these results by formalizing the choice of the appropriate data type (e.g., a tree structure) required to "implement" any given data type. This allows us to consider the formal implementation of a data type in terms of a concrete model.