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 compare and understand whether/why these techniques are sound, or to develop better techniques.
In this paper, we develop a unified framework to describe verification techniques for object invariants. We separate type system concerns from verification strategy concerns. We distil seven parameters that characterise a verification technique, and identify sufficient conditions on these parameters under which a verification technique is sound. 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 and expressiveness of these techniques.
Presented at FOOL'08; Sunday, 13 January 2007; San Francisco, California, USA.