Verification of Object-Oriented Programs with Invariants.
Mike Barnett, Robert A DeLine, Manuel A. Fähndrich, K. Rustan M. Leino, Wolfram Schulte · The Journal of Object Technology · 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 objectoriented 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.