appendix sectionnotation

Separation logic

symbol	meaning	first
symbol	meaning	first
$h_{1} # h_{2}$	heaps with disjoint domains	chapter 44
$h_{1} ⊎ h_{2}$	disjoint union of heaps	chapter 44
$E \mapsto F$	exact singleton points-to assertion	chapter 44
$P * Q$	separating conjunction on heap assertions, printed like BI multiplicative conjunction	chapter 44
$P - * Q$	separating implication, or magic wand, on heap assertions	chapter 44
$P ⊣⊢ Q$	mutual semantic entailment of heap assertions	chapter 44
$σ, h ⊧ P$	store–heap state satisfies assertion $P$	definition 44.3
$P ⊧ Q$	semantic inclusion between assertion denotations	proposition 44.5
$[[E {]]}_{σ}$	value of expression $E$ in store $σ$	definition 44.3
$h_{0} \subseteq h$	finite-map restriction of $h$	definition 44.1
$⟨ c, σ, h ⟩ ⇓ ⟨ σ^{'}, h^{'} ⟩$	big-step command execution	definition 44.6
$⊢ {P} c {Q}$	derivability in the local Hoare proof system	definition 44.15
$\mod (c)$	store variables assigned by $c$	chapter 44
$vars (c)$	every variable occurring in $c$	chapter 44
${chain}_{n} (x)$	exact $n$ -cell linked chain rooted at $x$	chapter 44