The Need for Flexible Object Invariants

Abstract

Specification and verification of object oriented programs usually features in some capacity the concept of an object invariant, used to describe the consistent states of an object. Unavoidably, an objects invariant will be broken at some points in its lifetime, and as a result, invariant protocols have been suggested, which prescribe the times at which object invariants may be broken, and the points at which they have to be re-established. The fact that currently available invariant protocols do not handle well some known examples, together with the fact that object invariants and invariant protocols can largely be encoded through methods pre- and post- conditions has recently raised the question of whether they still have a role to play, or should be replaced by more explicit pre- and post- conditions for methods. In this paper we argue that invariant protocols express programmers intuitions, lead to better design, allow more succinct specifications and proofs, and allow the expression of properties which involve many objects in a localised manner. In particular, the resulting verification conditions can be made simpler and more modular through the use of invariant-based reasoning. We also argue that even though encoding invariant protocols through methods pre- and post-conditions is possible, such an encoding loses important information, and as a result makes specifications less explicit and program evolution (whereby the program evolves after the encoding has taken place) more error-prone. Finally, we show that such encodings often cannot express properties over inaccessible objects, whereas an appropriate invariant protocol can handle them simply.