Behavioral Subtyping in Object-Oriented Languages by Krishna Kishore Dhara Abstract Modularity and code reuse are two important features of object-oriented programming. Modularity means that adding new components does not require reverifi- cation or respecification of existing components. A common form of reuse in objectoriented programs is to add new subtypes to existing types and to invoke already existing procedures with objects of these new types. In such cases, behavior of programs that contain these procedures also depend on the behavior of the new subtype objects. Reverifying the code that uses existing procedures whenever new types are added is not practical and is not modular. Thus, a notion of behavioral subtyping that allows sound modular reasoning is important for object-oriented programming. In this dissertation, we study behavioral subtyping for arbitrary abstract data types in the prescence of mutation and aliasing. We propose two notions of behavioral subtyping. Strong behavioral subtypes have objects that act like supertype objects in all cases, whereas as weak behavioral subtypes have objects that only need to act like supertype objects when manipulated as supertype objects. Both these notions allow sound modular reasoning based on the static types of variables in programs. Weak behavioral subtyping allows conclusions about programs based on the effects of individual procedures but restricts certain forms of aliasing. Strong behavioral subtyping allows all forms of aliasing but permits conclusions based only on the history constraints of the types. History constraints are the reflexive and transitive properties preserved by objects of a type across different states of a program. We prove that both these behavioral subtype notions are sufficient for sound modular reasoning. Keywords: object-oriented programming, behavioral subtype, abstract data type, mutation, aliasing, modular verification, supertype abstraction 1996 CR Categories: D.1.5 [Programming Techniques] Object-oriented Programming; D.3.1 [Programming Languages] Formal Definitions and Theory -- semantics; D.3.2 [Programming Languages] Language Classifications -- object-oriented languages; D.3.3 [Programming Languages] Language Constructs -- Abstract data types, modules, packages F.3.1 [Logics and Meanings of Programs] Specifying and Verifying and Reasoning about Porgrams -- logics of programs, pre- and post-conditions, theory