Validity Invariants and Effects

Object invariants describe the consistency of object states, and are crucial for reasoning about the correctness of object-oriented programs. However, reasoning about object invariants in the presence t abstraction and encapsulation, arbitrary object aliasing and re-entrant method calls, is difficult. We present a framework for reasoning about object invariants based on a behavioural contract that specifies two sets: the validity invariant-objects that must be valid before and after the behaviour; and the validity effect--objects that may be invalidated during the behaviour. The overlap of these two sets is critical because it captures precisely those objects that need to be re-validated at the end of the behaviour. When there is no overlap, no further validity checking is required. We also present a type system based on this framework using ownership types to confine dependencies for object invariants. In order to track the validity invariant, the type system restricts updates to perm...

• Type: Conference
• Year: 2007
• Where: ECOOP
• Authors: Yi Lu 0003, John Potter, Jingling Xue
• Keywords: ECOOP 2007, Object Invariants, Programming Languages, Re-entrant Method Calls, Reasoning