  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, we precisely connect the semantics of these two logics. We
define a logic whose syntax subsumes both that of a standard separation logic,
and that of implicit dynamic frames as sub-syntaxes. We define a total heap
semantics for our logic, and, for the separation logic subsyntax, prove it
equivalent the standard partial heaps model. In order to define a semantics
which works uniformly for both subsyntaxes, we define the novel concept of a
minimal state extension, which provides a different (but equivalent) definition
of the semantics of separation logic implication and magic wand connectives,
while also giving a suitable semantics for these connectives in implicit
dynamic frames. We show that our resulting semantics agrees with the existing
definition of weakest pre-condition semantics for the implicit dynamic frames
fragment. Finally, we show that we can encode the separation logic fragment of
our logic into the implicit dynamic frames fragment, preserving semantics. For
the connectives typically supported by tools, this shows that separation logic
can be faithfully encoded in a first-order automatic verification tool
(Chalice).
