Implementierungen Abstrakter Datentypen in terminaler Algebrasemantik

Abstract

In this paper we add a concept of implementation of abstract data types (adts) by adts in terminal algebra semantics to the notions of terminal algebra semantics of adts, which are introduced in [HR 79]. Our concept corresponds to that of initial implementations of adts described in [EKP 79a]. We give also a correctness proof of a T-implementation of stack (nat) by array (nat‚nat) as an application example for the methods developed in [HR 79]. As in [EKP 79a], the implementing data type is extended in two steps, called SORT-IMPLEMENTATION and OPERATIONS-IMPLEMENTATION, to take over the tasks of the implemented type. These two steps are syntactical constructions. The semantics of the T-implementation concept is layed down in the EXTENSION- and RESTRICTION-step. A third step of the initial case, called IDENTIFICATION, is not necessary here for reasons which result from the use of the terminal algebra semantics and which are explained in this paper. As in [EKP 79a], the concept of T-implementation distinguishes syntax, semantics and correctness.