Verifying Invariants in Object-Oriented Programs
- Rustan Leino ,
- Mike Barnett ,
- Robert DeLine ,
- Manuel Fähndrich ,
- Wolfram Schulte
Computer Science Colloquium, ETH Zurich |
- 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