An Exact Algebraic Characterization of Behavioral Subtyping

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. Submitted for publication. Copyright c fl Gary T. Leavens and Don Pigozzi, 1996. Department of Computer Science 226 Atanasoff Hall Iowa State University Ames, Iowa 50011-1040, USA Typeset by A M S-T E X ALGEBRAIC CHARACTERIZATION OF BEHAVIORAL SUBTYPING 1 AN EXACT ALGEBRAIC CHARACTERIZATION OF BEHAVIORAL SUBTYPING Gary T. Leavens and Don Pigozzi Iowa State University November 26, 1996 Abstract. A model theory for correct behavioral subtyping for abstract data types (with immutable objects) is developed within the framework of the behavior-realization adjunction. To allow for incomplete specifications, proofs of correct behavioral subtyping are based on comparison to one of several par..