Local Reasoning for Java

This thesis develops the local reasoning approach of separation logic for common forms of modularity such as abstract datatypes and objects. In particular, this thesis focuses on the modularity found in the Java programming language.

We begin by developing a formal semantics for a core imperative subset of Java, Middleweight Java (MJ), and then adapt separation logic to reason about this subset. However, a naive adaption of separation logic is unable to reason about encapsulation or inheritance: it provides no support for modularity.

First, we address the issue of encapsulation with the novel concept of an abstract predicate, which is the logical analogue of an abstract datatype. We demonstrate how this method can encapsulate state, and provide a mechanism for ownership transfer: the ability to transfer state safely between a module and its client. We also show how abstract predicates can be used to express the calling protocol of a class.

However, the encapsulation provided by abstract predicates is too restrictive for some applications. In particular, it cannot reason about multiple datatypes that have shared read-access to state, for example list iterators. To compensate, we alter the underlying model to allow the logic to express properties about read-only references to state. Additionally, we provide a model that allows both sharing and disjointness to be expressed directly in the logic.

Finally, we address the second modularity issue: inheritance. We do this by extending the concept of abstract predicates to abstract predicate families. This extension allows a predicate to have multiple definitions that are indexed by class, which allows subclasses to have a different internal representation while remaining behavioural subtypes. We demonstrate the usefulness of this concept by verifying a use of the visitor design pattern.