Separation Logic

Separation Logic is a refinement of Hoare Logic that adds the ability to reason about pointer manipulation, in particular Pointer Aliasing.

[2025-03-18 Tue]

Have an abstract set of heap addresses $\mathrm{Addr}$ , and a set of heaps $H$ which are indexed by Finite subsets of addresses. Also have a store, which maps variables to values.

$\par H=\bigcup_{A\subseteq\mathrm{Addr}}(A\rightharpoonup V)$

Alternatively, a heap is a Finitely Supported Partial Function $\mathrm{Addr}\rightharpoonup V$ .

Moreover, have a simple imperative language that is extended with allocation of cons cells, pointer dereferencing, pointer arithmetic, mutation, and deallocation.

Note that the expression language is separate from commands; this is similar to A Normal Form.

Logic is standard predicate calculus, plus:

$\mathrm{emp}$ , which asserts that a heap is empty; note that heap scoping is delimited by a Modality.
$a\mapsto e$ , which asserts that the heap contains one cell with address $a$ and contents $e$ .
$P*Q$ , which asserts taht the heap can be split into two disjoint halves such that $P$ holds for one part and $Q$ holds for the other.
$P\septo Q$ , which asserts that if the heap is extended by a disjoint part where $P$ holds, then $Q$ holds for the extended heap. This is a Right Adjoint to $P*Q$ .

Frame Rule

The all-important frame rule lets us lift a proof of a local property into a more global property, provided that $c$ does not touch the parts of the heap that the extended property mentions.

$\par\frac{\Hoare{P}{c}{Q}}{\Hoare{P*R}{c}{Q*R}}$

Examples

Reversing a List

struct list_t {
  int head;
  list_t *tail;
}

void reverse(list_t *i) {
  list_t *j = NULL;
  while (i != NULL) {
    list_t k = i->tail;
    i->tail = j;
    j = i;
    i = k;
  }
}

To prove that $\Hoare{\mathsf{list}\;\alpha_{0}\;i}{\mathrm{reverse(i)}}{\mathsf{list}\;% \alpha_{0}^{\dagger}\;j}$ (where $\alpha^{\dagger}$ is list reversal), the invariant

$\exists\alpha,\beta.\;\mathsf{list}\;\alpha\;i\land\mathsf{list}\;\beta\;j% \land\alpha_{0}^{\dagger}=\alpha^{\dagger}+\beta$

doesn't get you want you need due to aliasing concerns; instead, we need to use the the invariant

$(\exists\alpha,\beta.\;\mathsf{list}\;\alpha\;i*\mathsf{list}\;\beta\;j)\land% \alpha_{0}^{\dagger}=\alpha^{\dagger}+\beta$

where $P*Q$ is the separating conjunction, which asserts that the heap can be split into two disjoint halves where $P$ holds on one half and $Q$ holds on the other.