Separation Logic for Object-Oriented Programming
- Matthew J. Parkinson ,
- Gavin Bierman
in Aliasing in Object-Oriented Programming. Types, Analysis and Verification
Published by Springer | 2013, Vol 7850 | Aliasing in Object-Oriented Programming. Types, Analysis and Verification edition
In this article we propose techniques based on separation logic to reason about object-oriented programs. This leads to a modular proof system that can deal with features considered core to object-oriented programming, including object encapsulation, subclassing, inheritance, and dynamic dispatch.