Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Behavioral Subtyping, Specification Inheritance, and Modular Reasoning by Gary T. Leavens and David A. Naumann Abstract Verification of object-oriented programs that use subtyping and dynamic dispatch faces a fundamental difficulty: the behavior of a dynamically dispatched method call, such as E.m(), may vary depending on the dynamic type of the receiver, E. To avoid extensive use of case analysis in such verifications, and to allow new subtypes to be added to a program later, programmers often reason using supertype abstraction. With supertype abstraction, one reasons about a call such as E.m() using the specification given for the static type of E. Supertype abstraction is valid when each subtype in the program is a behavioral subtype (of all of its supertypes). However, for languages with references and mutable objects neither supertype abstraction nor behavioral subtyping has been rigorously formalized in isolation. The standard informal notions have inadequacies and exact definitions are not obvious. This paper formalizes supertype abstraction and two forms of behavioral subtyping for a Java-like sequential language with mutable heap objects, references, runtime type tests, exceptions, classes, interfaces, and recursive types. Specifications are treated semantically, independent from any particular assertion language or verification system. One form of behavioral subtyping is proved sound for reasoning with supertype abstraction and indeed equivalent to it (i.e., also semantically complete). Specification inheritance, as used in the specification language JML, is formalized and proved to entail the other, stronger form of behavioral subtyping. Categories and Subject Descriptors: D.2.2 [Software Engineering] Design Tools and Techniques --- Object-oriented design methods; D.2.3 [Software Engineering] Coding Tools and Techniques --- Object-oriented programming; D.2.4 [Software Engineering [Software/Program Verification --- Correctness proofs, formal methods, programming by contract, reliability, tools, Eiffel, JML; D.2.7 [Software Engineering] Distribution, Maintenance, and Enhancement --- Documentation; D.3.1 [Programming Languages] Definitions and Theory --- Semantics; D.3.2] Pro\-gram\-ming Languages] Language Classifications --- Object-oriented languages; D.3.3 [Programming Languages] Language Constructs and Features --- classes and objects, inheritance; F.3.1 [Logics and Meanings of Programs] Specifying and Verifying and Reasoning about Programs --- Assertions, logics of programs, pre- and post-conditions, specification techniques. General Terms: Specification, Verification Keywords: Behavioral subtyping, supertype abstraction, specification inheritance, modularity, specification, verification, refinement, state transformer, predicate transformer, dynamic dispatch, Eiffel language, JML language.