@article{barnett2004verification,
author = {Barnett, Mike and DeLIne, Robert and Fahndrich, Manuel and Leino, Rustan and Schulte, Wolfram},
title = {Verification of Object-Oriented Programs With Invariants},
year = {2004},
month = {June},
abstract = {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.},
url = {http://approjects.co.za/?big=en-us/research/publication/verification-of-object-oriented-programs-with-invariants-2/},
pages = {27-56},
journal = {Journal of Object Technology, Special issue},
volume = {3},
edition = {Journal of Object Technology, Special issue: ECOOP 2003 workshop on FTfJP},
number = {6},
note = {Published as Technical Report 408 from ETH Zurich.},
}