Verification of object-oriented programs with invariants

Mike Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, and Wolfram Schulte


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.


Publication typeArticle
Published inJournal of Object Technology
PublisherTechnical report 408, Department of Computer Science, ETH Zurich
> Publications > Verification of object-oriented programs with invariants