Behavioral Subtyping is Equivalent to Modular Reasoning for Object-oriented Programs
Gary T. Leavens, David A. Naumann · 2006
Abstract. Behavioral subtyping enables modular reasoning about the functional behavior of object-oriented programs. It validates supertype abstraction, that is, modular reasoning about dynamically dispatched method calls, such as E.m(), using specifications associated with their receiver’s static type, such as the static type of E. For languages with references and mutable objects neither behavioral subtyping nor supertype abstraction has been rigorously formalized as such. Moreover, the standard informal notion of behavioral subtyping has inadequacies. This paper gives a new formalization of behavioral subtyping and supertype abstraction, and a new proof of their equivalence. Our new formalization handles a realistic subset of sequential Java, with classes and interfaces, recursive types, and dynamically-allocated mutable objects.