Verification of object-oriented programs relies on object invariants to express consistency criteria of objects. The semantics of object invariants is subtle, mainly because of call-backs, multi-object invariants, and subclassing.
Several verification techniques for object invariants have been proposed. These techniques are complex and differ in restrictions on programs (for instance, which fields can be updated), restrictions on invariants (what an invariant may refer to), use of advanced type
systems (such as ownership types), meaning of invariants (in which execution states are invariants assumed to hold), and proof obligations (when should an invariant be proven). As a result, it is difficult to understand whether/why these techniques are sound, whether/why they are modular, and to compare their expressiveness. This general lack of understanding also hampers the development of new techniques.
In this paper, we develop and formalise a unified framework to describe verification techniques for object invariants. We distil seven parameters that characterise a verification technique, and identify sufficient conditions on these parameters under which a verification technique is sound. We also define what it means for a technique to be modular. To illustrate the generality of our framework, we instantiate it with six verification techniques from the literature. We show how our framework facilitates the assessment and comparison of the soundness, modularity, and expressiveness of these techniques.
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.