Verification of object-oriented programs with invariants

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.

verificationofobjectorientedprogramswithinvariants(jot2004).pdf
PDF file

In  Journal of Object Technology

Publisher  Technical report 408, Department of Computer Science, ETH Zurich

Details

TypeArticle
URLhttp://www.jot.fm/issues/issue_2004_06/article2
Pages27-56
Volume3
Number6
> Publications > Verification of object-oriented programs with invariants