IRUS Total

The Need for Flexible Object Invariants

File Description SizeFormat 
invariants-iwaco09.pdfAccepted version166.64 kBAdobe PDFView/Open
Title: The Need for Flexible Object Invariants
Authors: Summers, A
Drossopoulou, S
Müller, P
Item Type: Conference Paper
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.
Issue Date: 31-Jul-2009
URI: http://hdl.handle.net/10044/1/5954
Publisher Link: http://doi.acm.org/10.1145/1562154.1562160
ISBN: 978-1-60558-546-8
Publisher: ACM
Presented At: International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO) 2009
Published Proceedings: European Conference on Object-Oriented Programming
Copyright Statement: © 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.1562160
Conference Location: Genova, Italy
Appears in Collections:Computing
High Performance Informatics