The Behavior-Realization Adjunction and Generalized Homomorphic Relations by Gary T. Leavens and Don Pigozzi 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. 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.