Separation logic

Definition

Fix a set $\mathit{Var}$ of variables and a set $\mathit{Loc} \subseteq \Z$ of locations. A store is a function $s \colon \mathit{Var} \to \Z$, and a heap is a function $h \colon \mathrm{dom}(h) \to \Z$ with finite domain $\mathrm{dom}(h) \subseteq \mathit{Loc}$. Two heaps $h_1, h_2$ are disjoint if their domains are disjoint, and then $h_1 \cdot h_2$ is the heap on $\mathrm{dom}(h_1) \cup \mathrm{dom}(h_2)$ that agrees with each. The assertions of separation logic extend first-order formulas over the store with the following, and their meaning is a relation $s, h \models P$.

1. $s, h \models \mathsf{emp}$ if $\mathrm{dom}(h)$ is empty.
2. $s, h \models E \mapsto F$ if $\mathrm{dom}(h) = \set{s(E)}$ and $h(s(E)) = s(F)$, where $s(E)$ is the value of the expression $E$ in $s$.
3. $s, h \models P * Q$ if $h = h_1 \cdot h_2$ for some disjoint heaps with $s, h_1 \models P$ and $s, h_2 \models Q$.
4. $s, h \models P \mathrel{-\!\!*} Q$ if for every heap $h'$ disjoint from $h$ with $s, h' \models P$, also $s, h \cdot h' \models Q$.

Separation logic is the Hoare logic for a language with heap commands, with triples $\set{P}\, C\, \set{Q}$ over these assertions. Triples are read with fault avoidance. From any state satisfying $P$, the command $C$ never accesses a location outside the heap, and if it terminates, the final state satisfies $Q$. Its central rule is the frame rule: from $\set{P}\, C\, \set{Q}$ derive $\set{P * R}\, C\, \set{Q * R}$, provided $C$ assigns no variable that occurs free in $R$.