Leavens, Gary T. and Pigozzi, Don (1996) The Behavior-Realization Adjunction and Generalized. Technical Report TR94-18b, Department of Computer Science, Iowa State University.
The Behavior-Realization Adjunction
and Generalized Homomorphic Relations
Gary T. Leavens and Don Pigozzi
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.
Keywords: behavior, realization, observable equivalence,
simulation, generalized relation, abstract data type, model theory.
1994 CR Categories:
D.3.3 [Programming Languages]
Language Constructs --- Abstract data types;
F.3.2 [Logics and Meanings of Programs]
Semantics of Programming Languages --- algebraic approaches to semantics;
F.3.2 [Mathematical Logic and Formal Languages]
Mathematical Logic --- model theory.
1991 Mathematics Subject Classification.
Primary: 68Q65 Secondary: 68N05, 68N15, 68Q60.
Contact site administrator at: firstname.lastname@example.org