ECOOP 2003 WORKSHOP ON FORMAL TECHNIQUES FOR JAVA-LIKE PROGRAMS (FTfJP)

Verification of object-oriented programs with invariants

Mike Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, Wolfram Schulte
Microsoft Research, Redmond, WA, USA

space

PDF Icon
PDF Version

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 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.

Note: Due to the typographical sophistication of this article, no HTML version is available. Please use the PDF version.

About the authors

space Mike Barnett is a strong supporter of esoteric radio stations. That’s how he learns about the latest hip music before his teenagers do.

Robert DeLine is a gifted carpenter. He is known for his carefully constructed multi-level staircases.

Manuel Fähndrich is an architect of backyard dwellings for minors. Combining fun and safety, his creations stand up to any weather.

K. Rustan M. Leino is a starving musician. In order to support himself, he has a wife and four working children.

Wolfram Schulte is an avid bicyclist. Every day, he rides toward a destination uphill from his home.

Cite this article as follows: Mike Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, Wolfram Schulte: "Verification of object-oriented programs with invariants", in Journal of Object Technology, vol. 3, no. 6, Special issue: ECOOP 2003 workshop on Formal Techniques for Java-like Programs, June 2004, pp. 27-56. http://www.jot.fm/issues/issue_2004_06/article2