Finite heaps and local Hoare logic

Fix a countably infinite variable set $V$; each program and derivation uses only finitely many variables. Stores $\sigma :V\to \mathsf{Val}$ are total, and all syntax is well scoped over $V$. Heaps $h$ are finite partial maps from non-null locations to values. Write $h_1\mathrm{\#}{h}_2$ for disjoint domains and $h_1\uplus h_2$ for their disjoint union. Assertions are Their load-bearing heap clauses are Separating implication is the extension condition Pure equality and the Boolean connectives have their ordinary clauses, and $\mathrm{\exists }x.P$ ranges over values by store update. Separating conjunction has unit $\mathsf{emp}$ and is commutative and associative up to mutual entailment. If $S$ is pure, then $(P\ast Q)\wedge S$, $(P\wedge S)\ast Q$, and $P\ast (Q\wedge S)$ are mutually entailing.

Expressions are variables or literal values. Commands are The complete big-step semantics is

$⟨\mathsf{skip},\sigma ,h⟩\Downarrow ⟨\sigma ,h⟩$

$v=[[E{]]}_{\sigma }$

$⟨x:=E,\sigma ,h⟩\Downarrow ⟨\sigma [x\mapsto v],h⟩$

$\ell =[[E{]]}_{\sigma }$$h(\ell )=v$

$⟨x:=[E],\sigma ,h⟩\Downarrow ⟨\sigma [x\mapsto v],h⟩$

$\ell =[[E{]]}_{\sigma }$$\ell \in \mathrm{dom}(h)$$v=[[F{]]}_{\sigma }$

$⟨[E]:=F,\sigma ,h⟩\Downarrow ⟨\sigma ,h[\ell \mapsto v]⟩$

$v=[[E{]]}_{\sigma }$$\ell \notin \mathrm{dom}(h)$$\ell \ne \mathsf{null}$

$⟨x:=\mathsf{alloc}(E),\sigma ,h⟩\Downarrow ⟨\sigma [x\mapsto \ell ],h\uplus \{\ell \mapsto v\}⟩$

$\ell =[[E{]]}_{\sigma }$$\ell \in \mathrm{dom}(h)$

$⟨\mathsf{free}(E),\sigma ,h⟩\Downarrow ⟨\sigma ,h\upharpoonright (\mathrm{dom}(h)\setminus \{\ell \})⟩$

$⟨c_1,\sigma ,h⟩\Downarrow ⟨{\sigma }_1,h_1⟩$$⟨c_2,{\sigma }_1,h_1⟩\Downarrow ⟨{\sigma }_2,h_2⟩$

$⟨c_1;c_2,\sigma ,h⟩\Downarrow ⟨{\sigma }_2,h_2⟩$

$[[E{]]}_{\sigma }=[[F{]]}_{\sigma }$$⟨c_1,\sigma ,h⟩\Downarrow ⟨{\sigma }^{\prime },h^{\prime }⟩$

$⟨\mathsf{if}E=F\mathsf{then}{c}_1\mathsf{else}{c}_2,\sigma ,h⟩\Downarrow ⟨{\sigma }^{\prime },h^{\prime }⟩$

$[[E{]]}_{\sigma }\ne [[F{]]}_{\sigma }$$⟨c_2,\sigma ,h⟩\Downarrow ⟨{\sigma }^{\prime },h^{\prime }⟩$

$⟨\mathsf{if}E=F\mathsf{then}{c}_1\mathsf{else}{c}_2,\sigma ,h⟩\Downarrow ⟨{\sigma }^{\prime },h^{\prime }⟩$

Safety is structural: skip, assignment, and allocation are safe; load, store, and free require the evaluated address in the heap domain; a sequence requires the first command safe and the second safe after every first result; a conditional requires its selected branch safe. The set $\mathrm{mod}(c)$ contains all store variables assigned by $c$. The set $\mathrm{vars}(c)$ contains every variable occurrence in $c$, including assignment, load, and allocation targets:

A semantic triple $\{P\}c\{Q\}$ requires safety and $Q$ for every result from every state satisfying $P$. The proof judgment is generated by

$⊢\{P\}\mathsf{skip}\{P\}$

$⊢\{P[E/x]\}x:=E\{P\}$

$⊢\{P\}{c}_1\{R\}$$⊢\{R\}{c}_2\{Q\}$

$⊢\{P\}{c}_1;c_2\{Q\}$

$P^{\prime }\vDash P$$⊢\{P\}c\{Q\}$$Q\vDash Q^{\prime }$

$⊢\{P^{\prime }\}c\{Q^{\prime }\}$

$⊢\{P\}c\{Q\}$$a\notin \mathrm{vars}(c)\cup \mathrm{fv}(Q)$

$⊢\{\mathrm{\exists }a.P\}c\{Q\}$

$x\notin \mathrm{fv}(E,F)$

$⊢\{E\mapsto F\}x:=[E]\{E\mapsto F\wedge x=F\}$

$⊢\{E\mapsto -\}[E]:=F\{E\mapsto F\}$

$x\notin \mathrm{fv}(F)$

$⊢\{\mathsf{emp}\}x:=\mathsf{alloc}(F)\{x\mapsto F\}$

$⊢\{E\mapsto -\}\mathsf{free}(E)\{\mathsf{emp}\}$

$⊢\{P\wedge E=F\}{c}_1\{Q\}$$⊢\{P\wedge E\ne F\}{c}_2\{Q\}$

$⊢\{P\}\mathsf{if}E=F\mathsf{then}{c}_1\mathsf{else}{c}_2\{Q\}$

$⊢\{P\}c\{Q\}$$\mathrm{mod}(c)\cap \mathrm{fv}(R)=\varnothing$

$⊢\{P\ast R\}c\{Q\ast R\}$

The exact-chain family used by the running program is defined for expressions: $${\mathsf{chain}}_0(E)=\mathsf{emp}\wedge E=\mathsf{null},{\mathsf{chain}}_{n+1}(E)=\mathrm{\exists }a.E\mapsto a\ast {\mathsf{chain}}_n(a),$$ where $a$ is alpha-renamed away from the free variables and surrounding binders at every unfolding.

Assertion substitution is capture avoiding (lemma 44.14), and the fresh-variable coincidence lemma lemma 44.9 is the semantic premise behind H-Exists.