Separation Logic for Object-oriented Programs

Matthew Parkinson, Royal Academy of Engineering and EPSRC Research Fellow, University of Cambridge

In this course, we will develop a separation logic for a core sequential Java-like language. We will begin by showing how using separation logic predicates we can reason about abstract data types, and compare this approach to Hoare's original data abstraction paper. We will then illustrate the difficulties of combining object-oriented subtyping with separation logic, and present abstract predicate families as a solution to this. The logic will be extended to show how methods can be inherited without the need for reverification. Throughout, the logic will be illustrated with a series of simple examples about inheritance, and then a more detailed case study involving design patterns. Finally, we will discuss how this logic can be automated and present the jStar tool.