Technical Report Number
Theory of Computation, Data, Information Systems
A model theory for proving correctness of abstract data types is developed within the framework of the behavior-realization adjunction. To allow for incomplete specifications, proof-of-correctness is based on comparison to one of several paradigmatic models. For making such comparisons, the notions of the behavior and realization relations, and their duals are developed. These relations are used to give the first exact algebraic characterization of behavioral reduction and equivalence for algebras that are not term-generated.