Behavioral Subtyping is Equivalent to Modular Reasoning for Object-oriented Programs

摘要: Behavioral subtyping is an established idea that enables modular reasoning about behavioral properties of object-oriented programs. It requires syntactic subtypes are refinements. validates a dynamically-dispatched method call, say E .m(), using the specification associated with static type receiver expression . For languages references and mutable objects has not been rigorously formalized as such standard informal notion inadequacies. This paper formalizes introduces new formalization reasoning, called supertype abstraction. A Java-like sequential language considered, classes interfaces, recursive types, first-class exceptions handlers, dynamically allocated heap objects; semantics designed to serve foundation for Java Modeling Language (JML), widely used language. characterized sound semantically complete