Summers, AASummersDrossopoulou, SSDrossopoulouMüller, PPMüller2010-09-272010-09-272009-07European Conference on Object-Oriented Programming, 2009978-1-60558-546-8http://hdl.handle.net/10044/1/5954Specification 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 object's 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.\r\n\r\nThe 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.\r\n\r\nIn 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.\r\n\r\nWe 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.© ACM, 2009. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in EUROPEAN CONFERENCE ON OBJECT-ORIENTED PROGRAMMING, (2009) http://doi.acm.org/10.1145/1562154.1562160Conference Paperhttp://doi.acm.org/10.1145/1562154.1562160