| On the Role of Invariants in Reasoning about Object-Oriented Languages (2008) | |||||||||||||||
Abstract | |||||||||||||||
| 1 Introduction Preconditions, postconditions and invariants are universally accepted as the basic ingredients for specification of OO programs. Invariants for classes play an important role in object-oriented languages ([11,14]) because they often express key data integrity properties, such as: this integer field is always non-negative, or this reference is never null. The idea is that invariants should always hold. But things are not so simple. Consider for example the invariant i+j==0. It does not hold in between the two statements i++;j--, even though it will hold after the composition, assuming it holds before. It is inevitable that some invariants are temporarily invalidated in a method body, but they should be re-established at some point. | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||