Shared mutable objects are a cornerstone of the object-oriented paradigm. Modular reasoning remains a challenge. For example, how can a client of setLeftZero be certain that the right subtree did not change after the invocation?

In this talk, I will describe a program logic, called Region Logic, designed to control aliasing through explicit use of effects and disjointness assertions. The logic employs regions (sets of references) in a novel way, by using them in ghost state (i.e., as program annotations), effects and assertions. The region assertion language is especially instrumental in reasoning about many interesting “lightweight” specifications (e.g., without reachability predicates or inductive definitions).

To substantiate the preceding claim, I will present a specification (in Region Logic) derived from the Composite design pattern challenge problem and describe how to automatically verify it. Lastly, I will give some insight into a decision procedure for quantifier-free region assertions.