Publication Date

7-1996

Technical Report Number

TR94-18b

Subjects

Theory of Computation, Data, Information Systems

Abstract

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.

Comments

Copyright © Gary T. Leavens and Don Pigozzi, 1994, 1996. This copyright will be transferred to the journal.

Share

COinS