Verifying Invariants in Object-Oriented Programs - Leino, Rustan; Barnett, Mike; DeLine, Robert; Fähndrich, Manuel; Schulte, Wolfram (Computer Science Colloquium, ETH Zurich, 2003)
Invariants different from pre/post-conditions Resulting program invariants hold at every program point Uses pack/unpack commands, but good defaults can be constructed for these No linear type system Components are not unique references—objects (pointers) can freely be copied Fields can freely be read No additional features of abstraction needed to support the specification of modifications Sound