A Unified Framework for Verification Techniques for Object Invariants

Verification of object-oriented programs relies on object invariants which express consistency criteria of objects. The semantics of object invariants is subtle, mainly because of call-backs, multiobject invariants, and subclassing. Several verification techniques for object invariants have been proposed. These techniques are complex and differ in restrictions on programs (e.g., which fields can be updated), restrictions on invariants (what an invariant may refer to), use of advanced type systems (such as Universe types or ownership), 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 approaches. In this paper, we develop and formalise a unified framework to describe verificatio...

• Type: Conference
• Year: 2008
• Where: ECOOP
• Authors: Sophia Drossopoulou, Adrian Francalanza, Peter Müller, Alexander J. Summers
• Keywords: ECOOP 2008, Object Invariants, Programming Languages, Several Verification Techniques, Verification Techniques