The Relationship Between Separation Logic and Implicit Dynamic Frames
Separation logic is a concise method for specifying programs that manipulate dynamically allocated storage. Partially inspired by separation logic, Implicit Dynamic Frames has recently been proposed, aiming at first-order tool support. In this paper, the authors provide a total heap semantics for a standard separation logic, and prove it equivalent to the standard model. With small adaptations, they then show how to give a direct semantics to implicit dynamic frames and show this semantics correctly captures the existing definitions. This precisely connects the two logics. As a consequence of this connection, they show that a fragment of separation logic can be faithfully encoded in a first-order automatic verification tool (Chalice).