Verification of Object-Oriented Programs With Invariants - Barnett, Mike; DeLIne, Robert; Fahndrich, Manuel; Leino, Rustan; Schulte, Wolfram (Journal of Object Technology, Special issue, 2004)
An object invariant defines what it means for an object’s data to be in a consistent state. Object invariants are central to the design and correctness of object-oriented programs. This paper defines a programming methodology for using object invariants. The methodology, which enriches a program’s state space to express when each object invariant holds, deals with owned object components, ownership transfer, and subclassing, and is expressive enough to allow many interesting object-oriented programs to be specified and verified. Lending itself to sound modular verification, the methodology also provides a solution to the problem of determining what state a method is allowed to modify.
Published as Technical Report 408 from ETH Zurich.