The Need for Flexible Object Invariants
File(s)
Accepted version
Author(s)
Summers, A
Drossopoulou, S
Müller, P
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 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.
Date Issued
2009-07
Citation
European Conference on Object-Oriented Programming, 2009
ISBN
978-1-60558-546-8
Publisher
ACM
Source Title
International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO) 2009
Conference
European Conference on Object-Oriented Programming
Journal / Book Title
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
Identifier
http://www.cs.purdue.edu/homes/wrigstad/iwaco09/
Source
International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO) 2009
Source Place
Genova, Italy
Start Date
2009-07-07
Finish Date
2009-07-07
Coverage Spatial
Genova, Italy