Lambda the Ultimate

Validity Invariants and Effects, Yi Lu, John Potter and Jingling Xue. ECOOP 2007.

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 of object abstraction and encapsulation, arbitrary object aliasing and re-entrant method calls, is difficult. We present a general framework for reasoning about object invariants based on a behavioural abstraction that specifies two sets---the validity invariant, representing objects that must be valid before and after the behaviour, and the validity effect, describing 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. This system uses ownership types to confine dependencies for object invariants, and restricts permissible updates to track where object invariants hold even in the presence of re-entrant calls, but otherwise object referenceability and read access are not restricted.

I really liked this paper, but I think it might need a few preliminary explanations. There's a style of verification of OO programs based on "object invariants", which is the idea that you ensure that each object has an invariant, which every method maintains. Then verification is local, in the sense that you can verify each class's invariants independently. (This is used in the Boogie methodology used by Spec#, for instance.)

However, there are a couple of wrinkles. First, aliasing: every object's invariant depends on some of the objects in its fields, and you don't want random aliases letting strangers modify your representation objects underneath your feet. So you introduce a notion of ownership to help track who has permission to mess with each object. Second, reentrancy: suppose the middle of a method body has temporarily broken the object's invariant, and you call another method on the object? You don't a priori know the call is safe.

The type system the authors have introduced here tracks ownership and possibly-dangerous reentrant calls. The really clever part is that instead of just rejecting programs that fail these checks, they log all of the places where things break. So instead of saying "yes" or "no", the type system says "yes" or "manually verify the following things". So it's a labor-saving device for a verification methodology.