Subtyping, Modular Specification, and Modular Verification for Applicative Object-Oriented Programs
We present a formal specification language and a formal verification logic for a simple object-oriented programming language. The language is applicative and statically typed, and supports subtyping and message-passing. The verification logic relies on a behavioral notion of subtyping that captures the intuition that a subtype behaves like its supertypes. We give a formal definition for legal subtype relations, based on the specified behavior of objects, and show that this definition is sufficient to ensure the soundness of the verification logic. The verification logic reflects the way programmers reason informally about object-oriented programs, in that it allows them to use static type information, which avoids the need to consider all possible run-time subtypes. We also show that the logic does not require reverification of unchanged code when legal subtypes are added to a program.
© Gary T. Leavens and William E. Weihl, 1992, 1993, 1994. All rights reserved. Much of this report will appear in Acta Informatica, and so the copyright for those portions will be assumed by the Springer-Verlag.