When Separation Logic met Java

Опубликовано 7 сентября 2016, 16:24

Separation logic is a promising new approach to modular reasoning, but so far it has primarily been applied to low-level C-like languages. To extend separation logic to allow modular reasoning about object-oriented languages like Java, we must add encapsulation and behavioural subtyping to the logic. However, a naive integration of behavioural subtyping and separation logic is too restrictive. In this talk I will demonstrate how abstract predicate families provide an abstraction mechanism that addresses these restrictions, by mirroring dynamic dispatch in the logic. We demonstrate the utility of our approach with a series of examples, including the Visitor pattern.