Prerequisites. Direct starred prerequisites: Chapter 43. No later core chapter depends on this route.
A command that changes one heap cell should not have to re-establish a description of every other cell. Yet two variables can contain the same address. Knowing that each variable names a cell containing 1 does not show that there are two independently owned cells: both descriptions may name the same cell. What property of the heap distinguishes the two-cell state from this aliased one, and what condition ensures that a command changing one cell leaves the other cell untouched?
The heap split forced by aliasing
Let locations be natural numbers. Values are integers, locations, and the distinguished value 𝗇𝗎𝗅𝗅. Fix a countably infinite set 𝑉 of program variables. Each program, assertion, and derivation uses only finitely many of them, so every finite avoidance set admits a fresh auxiliary. A store 𝜎:𝑉→𝖵𝖺𝗅 is total. Every expression, assertion, and command is well scoped over 𝑉, and every assignment target lies in 𝑉. A heap ℎ is a finite partial map from non-null locations to values. Thus expression evaluation never fails; the load, store, and free commands are the only rules whose premises can fail because a heap address is absent.
Write ℎ1#ℎ2 when their domains are disjoint: dom(ℎ1)∩dom(ℎ2)=∅. When this holds, ℎ1⊎ℎ2 is their union. The empty heap is ∅. A subheapℎ0⊆ℎ is a restriction of ℎ. Its complement 𝑟, determined by ℎ=ℎ0⊎𝑟, is unique.
Whenever the displayed unions are defined, ℎ⊎∅=ℎ,ℎ1⊎ℎ2=ℎ2⊎ℎ1,(ℎ1⊎ℎ2)⊎ℎ3=ℎ1⊎(ℎ2⊎ℎ3). If ℎ=ℎ1⊎ℎ2=ℎ′1⊎ℎ′2, the two splittings need not agree. They do agree when either component is fixed as a subheap of ℎ.
Proof. The first three claims are the unit, commutativity, and associativity laws for disjoint finite-map union. For the last clause, a complement contains exactly the locations of ℎ that are absent from ℎ0, and it agrees with ℎ at every such location. Hence two complements are the same finite map. For nonuniqueness, let ℎ={1↦𝑎,2↦𝑏}. The ordered witnesses ({1↦𝑎},{2↦𝑏}) and (ℎ,∅) give different splittings of the same heap. The difference is not merely the commutativity of ⊎: their first components have different domains. ◻
Ordinary conjunction observes one heap twice. A separating conjunction divides the heap into disjoint subheaps and checks one conjunct on each part.
A heap assertion is a formula generated by 𝑃,𝑄::=𝗍𝗋𝗎𝖾∣𝖿𝖺𝗅𝗌𝖾∣𝐸=𝐹∣𝐸≠𝐹∣𝖾𝗆𝗉∣𝐸↦𝐹∣𝑃∧𝑄∣𝑃∨𝑄∣𝑃∗𝑄∣𝑃−∗𝑄∣∃𝑥.𝑃. They denote sets of store–heap pairs. Write 𝜎,ℎ⊧𝑃 for membership in that denotation, and [[𝐸]]𝜎 for the value of the expression 𝐸 in the store 𝜎. Here 𝑃∗𝑄 is the separating conjunction introduced above, and 𝑃−∗𝑄 is separating implication, the assertion that every disjoint extension satisfying 𝑃 produces a combined heap satisfying 𝑄. These connectives print like the BI connectives of chapter 43, but their operands are heap assertions. The finite-heap algebra uses exact disjoint union rather than a preordered resource witness; the separate macros record that specialization. The clauses that mention the heap are below. In the points-to clause, put ℓ=[[𝐸]]𝜎 and 𝑣=[[𝐹]]𝜎. 𝜎,ℎ⊧𝗍𝗋𝗎𝖾⟺always,𝜎,ℎ⊧𝖿𝖺𝗅𝗌𝖾⟺never,𝜎,ℎ⊧𝐸=𝐹⟺[[𝐸]]𝜎=[[𝐹]]𝜎,𝜎,ℎ⊧𝐸≠𝐹⟺[[𝐸]]𝜎≠[[𝐹]]𝜎,𝜎,ℎ⊧𝖾𝗆𝗉⟺ℎ=∅,𝜎,ℎ⊧𝐸↦𝐹⟺ℓisanon-nulllocation∧ℎ={ℓ↦𝑣},𝜎,ℎ⊧𝑃∗𝑄⟺∃ℎ1,ℎ2.ℎ=ℎ1⊎ℎ2∧𝜎,ℎ1⊧𝑃∧𝜎,ℎ2⊧𝑄,𝜎,ℎ⊧𝑃∧𝑄⟺𝜎,ℎ⊧𝑃∧𝜎,ℎ⊧𝑄,𝜎,ℎ⊧𝑃∨𝑄⟺𝜎,ℎ⊧𝑃∨𝜎,ℎ⊧𝑄,𝜎,ℎ⊧𝑃−∗𝑄⟺∀𝑟.(ℎ#𝑟∧𝜎,𝑟⊧𝑃⟹𝜎,ℎ⊎𝑟⊧𝑄),𝜎,ℎ⊧∃𝑥.𝑃⟺∃𝑣∈𝖵𝖺𝗅.𝜎[𝑥↦𝑣],ℎ⊧𝑃. Here expressions are variables or literal values. The assertion 𝐸↦− abbreviates ∃𝑧.𝐸↦𝑧, where 𝑧∈𝑉∖fv(𝐸). Free variables satisfy fv(𝖾𝗆𝗉)=∅,fv(𝐸=𝐹)=fv(𝐸)∪fv(𝐹),fv(𝐸↦𝐹)=fv(𝐸)∪fv(𝐹),fv(𝑃⋄𝑄)=fv(𝑃)∪fv(𝑄),fv(∃𝑥.𝑃)=fv(𝑃)∖{𝑥},fv(𝐸↦−)=fv(𝐸), where ⋄∈{∧,∨,∗,−∗}.
Proof. For the unit, the 𝖾𝗆𝗉 component is ∅, so its complement is the original heap. Commutativity and associativity transport the witnessing heap split along the corresponding laws of lemma 44.2. For the last display, suppose ℎ=ℎ1⊎ℎ2. Because 𝑆 ignores the heap, 𝜎,ℎ⊧𝑆, 𝜎,ℎ1⊧𝑆, and 𝜎,ℎ2⊧𝑆 are equivalent. The same split therefore moves the pure conjunct to either component; the converse uses the identical argument. ◻
The singleton in the points-to clause is essential. Thus 𝑥↦1∗𝑦↦2 entails 𝑥≠𝑦, while (𝑥↦1)∧(𝑦↦2) is false even when 𝑥≠𝑦: one heap cannot be two different singletons.
Proof of Proposition 44.5 — The separating adjunction
Proof. Suppose 𝑃∗𝑄⊧𝑅, and let 𝜎,ℎ⊧𝑃. For any 𝑟 disjoint from ℎ with 𝜎,𝑟⊧𝑄, the union ℎ⊎𝑟 satisfies 𝑃∗𝑄, hence 𝑅. Therefore 𝜎,ℎ⊧𝑄−∗𝑅.
Conversely, suppose 𝑃⊧𝑄−∗𝑅 and 𝜎,ℎ⊧𝑃∗𝑄. Choose ℎ=ℎ1⊎ℎ2 with 𝑃 on ℎ1 and 𝑄 on ℎ2. The premise gives 𝑄−∗𝑅 on ℎ1; applying its definition to ℎ2 gives 𝑅 on ℎ. ◻
Expressions 𝐸,𝐹 are variables or literal values. The following grammar therefore keeps expression evaluation separate from the heap operations: 𝑐::=𝗌𝗄𝗂𝗉∣𝑥:=𝐸∣𝑥:=[𝐸]∣[𝐸]:=𝐹∣𝑥:=𝖺𝗅𝗅𝗈𝖼(𝐸)∣𝖿𝗋𝖾𝖾(𝐸)∣𝑐1;𝑐2∣𝗂𝖿𝐸=𝐹𝗍𝗁𝖾𝗇𝑐1𝖾𝗅𝗌𝖾𝑐2. The big-step judgment ⟨𝑐,𝜎,ℎ⟩⇓⟨𝜎′,ℎ′⟩ is generated by the following rules. Store update is written 𝜎[𝑥↦𝑣], and heap update by ℎ[ℓ↦𝑣].
⟨𝗌𝗄𝗂𝗉,𝜎,ℎ⟩⇓⟨𝜎,ℎ⟩
E-Skip
𝑣=[[𝐸]]𝜎
⟨𝑥:=𝐸,𝜎,ℎ⟩⇓⟨𝜎[𝑥↦𝑣],ℎ⟩
E-Assign
ℓ=[[𝐸]]𝜎ℎ(ℓ)=𝑣
⟨𝑥:=[𝐸],𝜎,ℎ⟩⇓⟨𝜎[𝑥↦𝑣],ℎ⟩
E-Load
ℓ=[[𝐸]]𝜎ℓ∈dom(ℎ)𝑣=[[𝐹]]𝜎
⟨[𝐸]:=𝐹,𝜎,ℎ⟩⇓⟨𝜎,ℎ[ℓ↦𝑣]⟩
E-Store
𝑣=[[𝐸]]𝜎ℓ∉dom(ℎ)ℓ≠𝗇𝗎𝗅𝗅
⟨𝑥:=𝖺𝗅𝗅𝗈𝖼(𝐸),𝜎,ℎ⟩⇓⟨𝜎[𝑥↦ℓ],ℎ⊎{ℓ↦𝑣}⟩
E-Alloc
ℓ=[[𝐸]]𝜎ℓ∈dom(ℎ)
⟨𝖿𝗋𝖾𝖾(𝐸),𝜎,ℎ⟩⇓⟨𝜎,ℎ↾(dom(ℎ)∖{ℓ})⟩
E-Free
⟨𝑐1,𝜎,ℎ⟩⇓⟨𝜎1,ℎ1⟩⟨𝑐2,𝜎1,ℎ1⟩⇓⟨𝜎2,ℎ2⟩
⟨𝑐1;𝑐2,𝜎,ℎ⟩⇓⟨𝜎2,ℎ2⟩
E-Seq
[[𝐸]]𝜎=[[𝐹]]𝜎⟨𝑐1,𝜎,ℎ⟩⇓⟨𝜎′,ℎ′⟩
⟨𝗂𝖿𝐸=𝐹𝗍𝗁𝖾𝗇𝑐1𝖾𝗅𝗌𝖾𝑐2,𝜎,ℎ⟩⇓⟨𝜎′,ℎ′⟩
E-IfT
[[𝐸]]𝜎≠[[𝐹]]𝜎⟨𝑐2,𝜎,ℎ⟩⇓⟨𝜎′,ℎ′⟩
⟨𝗂𝖿𝐸=𝐹𝗍𝗁𝖾𝗇𝑐1𝖾𝗅𝗌𝖾𝑐2,𝜎,ℎ⟩⇓⟨𝜎′,ℎ′⟩
E-IfF
Allocation is nondeterministic only in the fresh location chosen.
Absence of a big-step derivation could mean either a fault or divergence in a larger language. This language has no loops, so we define safety directly and do not rely on that coincidence.
Safety is defined by structural recursion on commands:
𝗌𝗄𝗂𝗉, assignment, and allocation are safe;
load, store, and free are safe exactly when their evaluated address is in the heap domain;
𝑐1;𝑐2 is safe when 𝑐1 is safe and 𝑐2 is safe after every result of 𝑐1;
a conditional is safe when its selected branch is safe.
The finite set mod(𝑐) contains variables assigned by 𝑐, including load and allocation targets, and is combined by union for compound commands. The set vars(𝑐) contains every variable occurring anywhere in 𝑐, including assignment targets: vars(𝗌𝗄𝗂𝗉)=∅,vars(𝑥:=𝐸)={𝑥}∪fv(𝐸),vars(𝑥:=[𝐸])={𝑥}∪fv(𝐸),vars(𝑥:=𝖺𝗅𝗅𝗈𝖼(𝐸))={𝑥}∪fv(𝐸),vars([𝐸]:=𝐹)=fv(𝐸,𝐹),vars(𝖿𝗋𝖾𝖾(𝐸))=fv(𝐸),vars(𝑐1;𝑐2)=vars(𝑐1)∪vars(𝑐2),vars(𝗂𝖿𝐸=𝐹𝗍𝗁𝖾𝗇𝑐1𝖾𝗅𝗌𝖾𝑐2)=fv(𝐸,𝐹)∪vars(𝑐1)∪vars(𝑐2).
The program 𝖿𝗋𝖾𝖾(𝑥);𝑦:=[𝑥] is unsafe on every heap satisfying 𝑥↦𝑣. The first command removes the only cell; the address premise of the second is then false. This is a formal use-after-free, not a claim about how a particular machine manifests the error.
Proof of Lemma 44.8 — Commands change only modified variables
Proof. Induct on the execution derivation. The primitive cases inspect the one possible store update. Sequence uses the induction hypothesis twice and the definition of mod(𝑐1;𝑐2). A conditional uses the induction hypothesis for the selected branch. The assertion consequence is an induction on the assertion syntax; points-to and pure atoms evaluate the same expressions because none of their free variables changed. Separating connectives preserve the same heap splits. ◻
Let 𝑎∉vars(𝑐), and let stores 𝜎,𝜌 agree on every variable other than 𝑎. Then:
𝑐 is safe on (𝜎,ℎ) iff it is safe on (𝜌,ℎ);
every execution ⟨𝑐,𝜎,ℎ⟩⇓⟨𝜎′,ℎ′⟩ has a matching execution ⟨𝑐,𝜌,ℎ⟩⇓⟨𝜌′,ℎ′⟩, and the result stores agree away from 𝑎, with the converse correspondence as well; and
Proof. Prove the first two clauses simultaneously by structural induction on 𝑐. Every expression in a primitive command has the same value in the two stores. A store update has the same target and value, and its target is not 𝑎. The heap operations therefore have identical domain tests and heap results. In the allocation case choose the same fresh location in the matching execution. Sequence composes the two correspondences at the intermediate state, and a conditional selects the same branch. The safety clauses follow from the identical address tests and the induction hypotheses.
For the third clause, induct on 𝑃. Pure atoms and points-to inspect only their free variables; the propositional and separating connectives preserve the same truth values and heap splits. For ∃𝑥.𝑃, alpha-rename 𝑥 away from 𝑎 and use the same witness in both stores. ◻
Locality and the frame theorem
Locality is the requirement that adjoining a disjoint frame neither creates a fault nor permits that frame to be modified invisibly.
The tempting forward factorization is false for allocation: ⟨𝑥:=𝖺𝗅𝗅𝗈𝖼(𝐸),𝜎,ℎ0⟩⇓⟨𝜎[𝑥↦ℓ],ℎ0⊎{ℓ↦𝑣}⟩⟹̸⟨𝑥:=𝖺𝗅𝗅𝗈𝖼(𝐸),𝜎,ℎ0⊎𝑟⟩⇓⟨𝜎[𝑥↦ℓ],ℎ0⊎𝑟⊎{ℓ↦𝑣}⟩. Choose ℓ∈dom(𝑟)∖dom(ℎ0). The small allocation may choose ℓ, but the proposed large result is not a heap because the union is not disjoint. The repair reads a given large execution back to the footprint, so its chosen location is already fresh for the frame.
Proof of Theorem 44.11 — Locality of the command language
Proof. Proceed by structural induction on 𝑐, proving both clauses together. Skip and assignment do not change the heap. For load, store, and free, safety on ℎ0 says that the addressed location belongs to dom(ℎ0); disjointness ensures it does not belong to 𝑟. The large execution therefore reads, changes, or removes exactly the same cell of ℎ0, and finite-map algebra factors the result as the changed footprint united with 𝑟.
For allocation, safety is automatic. Suppose the large execution chooses ℓ∉dom(ℎ0⊎𝑟). Then ℓ is fresh for both components. The small execution may choose the same ℓ, and (ℎ0⊎𝑟)⊎{ℓ↦𝑣}=(ℎ0⊎{ℓ↦𝑣})⊎𝑟.
For a sequence, safety of 𝑐1;𝑐2 entails safety of 𝑐1 and safety of 𝑐2 after every small result of 𝑐1. Apply the induction hypothesis for 𝑐1 to factor the intermediate large result as ℎ1⊎𝑟. Its corresponding small result is one quantified over in the safety clause, so the induction hypothesis for 𝑐2 applies and factors the final result. The conditional selects the same branch on both heaps because its expressions depend only on the store; apply the induction hypothesis to that branch. ◻
The assertion {𝑃}𝑐{𝑄} is a semantic Hoare triple when the following conditions hold. For every 𝜎,ℎ satisfying 𝑃, the command 𝑐 is safe on (𝜎,ℎ). Every result ⟨𝑐,𝜎,ℎ⟩⇓⟨𝜎′,ℎ′⟩ satisfies 𝜎′,ℎ′⊧𝑄. This is partial correctness plus fault freedom. It makes no termination claim for a language containing loops or recursion.
Proof. Let 𝜎,ℎ⊧𝑃∗𝑅. Choose ℎ=ℎ0⊎𝑟 with 𝜎,ℎ0⊧𝑃 and 𝜎,𝑟⊧𝑅. Validity of {𝑃}𝑐{𝑄} gives safety on (𝜎,ℎ0); locality then gives safety on (𝜎,ℎ).
For any large result ⟨𝜎′,𝐻⟩, locality gives a small result ⟨𝜎′,ℎ′0⟩ with 𝐻=ℎ′0⊎𝑟. The premise triple gives 𝜎′,ℎ′0⊧𝑄. By lemma 44.8, 𝜎′,𝑟⊧𝑅, since variables free in 𝑅 were not modified. The displayed split therefore witnesses 𝜎′,𝐻⊧𝑄∗𝑅. ◻
The side condition is not decorative. From {𝗍𝗋𝗎𝖾}𝑥:=0{𝑥=0} one may not frame 𝑥=1: the command changes the store fact even though it changes no heap cell.
★☆☆ Use a one-variable store to show that deleting the free-variable side condition from theorem 44.13 derives an invalid triple. Identify the exact line of the proof that then fails.
Proof. Induct on 𝑃. Equality, disequality, and points-to use the ordinary expression-substitution calculation; the heap is unchanged. Boolean and separating connectives apply the induction hypotheses to the same heap or to each component of the same split. For ∃𝑦.𝑃, alpha-rename 𝑦 away from 𝑥 and fv(𝐸), then use the same witness on both sides. These cases exhaust definition 44.3. ◻
The adjunction now gives a backward-reasoning use of the wand. Frame (𝐸↦𝐹)−∗𝑄 around H-Store; its postcondition is (𝐸↦𝐹)∗((𝐸↦𝐹)−∗𝑄)⊧𝑄 by the counit direction of proposition 44.5. Hence ⊢{𝐸↦−∗((𝐸↦𝐹)−∗𝑄)}[𝐸]:=𝐹{𝑄}.
The conditional rules are exercised by a guarded load. For distinct variables 𝑥,𝑦, fix a value 𝑣 and put 𝑃𝑣=(𝑥=𝗇𝗎𝗅𝗅∧𝖾𝗆𝗉)∨(𝑥≠𝗇𝗎𝗅𝗅∧𝑥↦𝑣),𝑄𝑣=(𝑥=𝗇𝗎𝗅𝗅∧𝖾𝗆𝗉∧𝑦=0)∨(𝑥≠𝗇𝗎𝗅𝗅∧𝑥↦𝑣∧𝑦=𝑣),𝑔=𝗂𝖿𝑥=𝗇𝗎𝗅𝗅𝗍𝗁𝖾𝗇𝑦:=0𝖾𝗅𝗌𝖾𝑦:=[𝑥]. The true premise of H-If follows from H-Assign and consequence: 𝑃𝑣∧𝑥=𝗇𝗎𝗅𝗅⊧𝖾𝗆𝗉∧𝑥=𝗇𝗎𝗅𝗅. Rule H-Assign gives the actual triple ⊢{𝖾𝗆𝗉∧𝑥=𝗇𝗎𝗅𝗅}𝑦:=0{𝖾𝗆𝗉∧𝑥=𝗇𝗎𝗅𝗅∧𝑦=0}, whose postcondition entails 𝑄𝑣. The false premise begins with 𝑃𝑣∧𝑥≠𝗇𝗎𝗅𝗅⊧𝑥↦𝑣. Rule H-Load gives ⊢{𝑥↦𝑣}𝑦:=[𝑥]{𝑥↦𝑣∧𝑦=𝑣}, and its postcondition entails 𝑄𝑣. Consequence supplies both premises. Therefore H-If derives ⊢{𝑃𝑣}𝑔{𝑄𝑣}. Operationally, E-IfT followed by E-Assign handles 𝜎(𝑥)=𝗇𝗎𝗅𝗅,ℎ=∅; E-IfF followed by E-Load handles 𝜎(𝑥)=ℓ,ℎ={ℓ↦𝑣}. Thus all three conditional rules occur in a complete verification and its two executions.
Proof of Theorem 44.16 — Soundness of local Hoare reasoning
Proof. Induct on the derivation of ⊢{𝑃}𝑐{𝑄}. Skip follows from E-Skip. For assignment, semantic substitution and E-Assign give 𝜎,ℎ⊧𝑃[𝐸/𝑥]⟹𝜎[𝑥↦[[𝐸]]𝜎],ℎ⊧𝑃. For load, write ℓ=[[𝐸]]𝜎 and 𝑣=[[𝐹]]𝜎. The precondition means ℎ={ℓ↦𝑣}, so E-Load returns (𝜎[𝑥↦𝑣],ℎ). Since 𝑥∉fv(𝐸,𝐹), both expression values are unchanged, and the result satisfies 𝐸↦𝐹∧𝑥=𝐹. For store, E-Store changes {ℓ↦𝑣} to {ℓ↦[[𝐹]]𝜎}; for free, E-Free removes the unique cell and leaves ∅. For allocation, E-Alloc chooses ℓ∉dom(ℎ), extends the heap by {ℓ↦[[𝐹]]𝜎}, and stores ℓ in 𝑥. Under the rule’s precondition ℎ=∅, and 𝑥∉fv(𝐹) preserves the allocated value, so the result satisfies 𝑥↦𝐹.
In the sequence case, validity of the first premise gives safety and 𝑅 for every intermediate result. Validity of the second premise therefore gives safety and 𝑄 for every continuation. This is exactly the recursive safety clause for sequence and rule E-Seq. Consequence uses semantic inclusion. For H-Exists, choose the witness value in the precondition and apply the premise triple in the witness-updated store. Parts 1 and 2 of lemma 44.9 transfer safety and every execution back to the original store; part 3 transfers the postcondition because the auxiliary is not free in it. The conditional evaluates the same pure comparison as its operational rule, so the matching premise applies. The frame case is theorem 44.13, using locality of the command language. ◻
If 𝑡∉fv(𝑥↦𝑎∗𝑦↦𝑏)∪fv(𝑥↦𝑏∗𝑦↦𝑎), then ⊢{𝑥↦𝑎∗𝑦↦𝑏}𝑡:=[𝑥];[𝑥]:=𝑏;[𝑦]:=𝑡{𝑥↦𝑏∗𝑦↦𝑎}. In particular, the precondition entails 𝑥≠𝑦; no separate alias test is needed at run time.
Proof of Proposition 44.17 — Swapping two disjoint cells
Proof. The proof outline records every command between its precondition and postcondition: {𝑥↦𝑎∗𝑦↦𝑏}𝑡:=[𝑥];𝐻−𝐿𝑜𝑎𝑑+𝐻−𝐹𝑟𝑎𝑚𝑒{𝑥↦𝑎∗(𝑦↦𝑏∧𝑡=𝑎)}[𝑥]:=𝑏;𝐻−𝑆𝑡𝑜𝑟𝑒+𝐻−𝐹𝑟𝑎𝑚𝑒{𝑥↦𝑏∗(𝑦↦𝑏∧𝑡=𝑎)}[𝑦]:=𝑡𝐻−𝑆𝑡𝑜𝑟𝑒+𝐻−𝐹𝑟𝑎𝑚𝑒{𝑥↦𝑏∗𝑦↦𝑎}. Frame 𝑦↦𝑏 around H-Load. Freshness of 𝑡 yields 𝑥↦𝑎∗𝑦↦𝑏∧𝑡=𝑎. By the pure-redistribution and commutativity laws of proposition 44.4, this is equivalent to 𝑥↦𝑎∗(𝑦↦𝑏∧𝑡=𝑎). Frame that entire second factor around H-Store for [𝑥]:=𝑏, obtaining 𝑥↦𝑏∗𝑦↦𝑏∧𝑡=𝑎. For the final store, frame 𝑥↦𝑏∧𝑡=𝑎 around the axiom for [𝑦]:=𝑡, again using pure redistribution. The equality is therefore still available, and consequence rewrites the stored value from 𝑡 to 𝑎. Two applications of H-Seq join the three commands. The disjoint heap split in the initial star forces the two addresses to differ. ◻
A linked chain, one cell at a time
The running structure stores only a next pointer. This is enough to expose allocation, deallocation, and the role of separation.
For any expression 𝐸, define assertions by primitive recursion on 𝑛: 𝖼𝗁𝖺𝗂𝗇0(𝐸):=𝖾𝗆𝗉∧𝐸=𝗇𝗎𝗅𝗅,𝖼𝗁𝖺𝗂𝗇𝑛+1(𝐸):=∃𝑎.𝐸↦𝑎∗𝖼𝗁𝖺𝗂𝗇𝑛(𝑎). At each unfolding, the bound variable 𝑎 is alpha-renamed away from fv(𝐸) and every binder already in its scope. Thus 𝖼𝗁𝖺𝗂𝗇𝑛(𝐸) is the capture-avoiding instance at 𝐸. Each successor step consumes one cell disjoint from the tail.
If 𝜎,ℎ⊧𝖼𝗁𝖺𝗂𝗇𝑛(𝑥), its heap has exactly 𝑛 locations. At 𝑛=0 the head is null; at 𝑛>0 it is a non-null member of the heap domain. No location is reused along the recursive tail. Consequently, the cyclic singleton {ℓ↦ℓ} satisfies no 𝖼𝗁𝖺𝗂𝗇𝑛(ℓ).
Proof. Induct on 𝑛. At zero, the definition gives the empty heap and 𝑥=𝗇𝗎𝗅𝗅. At a successor, alpha-rename the displayed binder 𝑎 away from 𝑥, choose its witness value 𝑣, and choose the split ℎ={𝜎(𝑥)↦𝑣}⊎ℎ′,𝜎[𝑎↦𝑣],ℎ′⊧𝖼𝗁𝖺𝗂𝗇𝑛(𝑎). Exact points-to and the induction hypothesis give 𝜎(𝑥)≠𝗇𝗎𝗅𝗅,|dom(ℎ′)|=𝑛. Disjointness then gives 𝜎(𝑥)∉dom(ℎ′),|dom(ℎ)|=𝑛+1. Thus no location is reused. For the final claim, zero fails because the cyclic singleton is not empty. At a successor, the head consumes its only cell, leaving the empty heap with the same non-null tail head. The tail cannot be a zero chain because its head is not null, and cannot be a positive chain because its head is absent from the empty domain. ◻
Proof. Rule H-Alloc, framed by 𝖼𝗁𝖺𝗂𝗇𝑛(𝑥), gives {𝖾𝗆𝗉∗𝖼𝗁𝖺𝗂𝗇𝑛(𝑥)}𝑧:=𝖺𝗅𝗅𝗈𝖼(𝑥){𝑧↦𝑥∗𝖼𝗁𝖺𝗂𝗇𝑛(𝑥)}. By proposition 44.4, the precondition is equivalent to 𝖼𝗁𝖺𝗂𝗇𝑛(𝑥). Before the assignment 𝑥:=𝑧, the precondition required by H-Assign for postcondition 𝖼𝗁𝖺𝗂𝗇𝑛+1(𝑥) is 𝖼𝗁𝖺𝗂𝗇𝑛+1(𝑧). The displayed assertion entails it by choosing the old value of 𝑥 as the existential tail pointer. Sequence and consequence finish the derivation. ◻
Proof. Unfold the precondition and alpha-rename its witness variable 𝑎 away from 𝑥 and 𝑧: 𝑥↦𝑎∗𝖼𝗁𝖺𝗂𝗇𝑛(𝑎). The complete outline is {𝑥↦𝑎∗𝖼𝗁𝖺𝗂𝗇𝑛(𝑎)}𝑧:=[𝑥];𝐻−𝐿𝑜𝑎𝑑+𝐻−𝐹𝑟𝑎𝑚𝑒{𝑥↦𝑎∗(𝖼𝗁𝖺𝗂𝗇𝑛(𝑎)∧𝑧=𝑎)}𝖿𝗋𝖾𝖾(𝑥);𝐻−𝐹𝑟𝑒𝑒+𝐻−𝐹𝑟𝑎𝑚𝑒{𝖼𝗁𝖺𝗂𝗇𝑛(𝑎)∧𝑧=𝑎}𝑥:=𝑧𝐻−𝐴𝑠𝑠𝑖𝑔𝑛{𝖼𝗁𝖺𝗂𝗇𝑛(𝑥)}. Frame 𝖼𝗁𝖺𝗂𝗇𝑛(𝑎) around H-Load. The result is 𝑥↦𝑎∗𝖼𝗁𝖺𝗂𝗇𝑛(𝑎)∧𝑧=𝑎. By consequence, rewrite the last assertion as 𝑥↦𝑎∗(𝖼𝗁𝖺𝗂𝗇𝑛(𝑎)∧𝑧=𝑎), and frame the entire second factor around H-Free. The footprint cell disappears, leaving 𝖼𝗁𝖺𝗂𝗇𝑛(𝑎)∧𝑧=𝑎. This entails the assignment precondition 𝖼𝗁𝖺𝗂𝗇𝑛(𝑧) for the final command 𝑥:=𝑧. Rule H-Seq combines the three derivations, and H-Exists discharges the chosen auxiliary 𝑎. ◻
The ordinary-conjunction invariant 𝑥↦𝑎∧𝖼𝗁𝖺𝗂𝗇𝑛(𝑎) cannot support this proof. Its two parts demand the same whole heap, and it neither isolates the cell freed by 𝗉𝗈𝗉 nor proves that the tail survives.
For the finite sequential command language, a derivable triple establishes fault freedom and its postcondition for every terminating execution from a state satisfying the precondition. Framed heap cells are unchanged, and framed store facts are unchanged when the modified-variable side condition holds.
Proof. Soundness is theorem 44.16. The unchanged-heap conclusion is the factorization clause of locality used in theorem 44.13; the store conclusion is lemma 44.8. ◻
Proposition 44.22 is a partial-correctness and fault-freedom result for terminating executions. It contains no loop variant, no interference relation for concurrent steps, and no condition requiring a postcondition to retain every allocated cell. The assertion 𝑃∗𝑄 records only a semantic heap split.
Source note.
O’Hearn, Reynolds, and Yang give the small axioms and frame rule in Section 3, derive larger-footprint laws in Section 4, and isolate the fault-avoiding partial-correctness reading in Section 8 [ORY01]. Reynolds develops the same ingredients together with linked-list examples [Rey02]. The rules in definition 44.15 replay that order: exact one-cell axioms first, then framing and sequencing, and finally the linked-chain proofs of proposition 44.20, proposition 44.21.
The archived Separation Logic Foundations development supplies a mechanized comparison route [Cha25]. The declarations line up as follows; appendix D records the pinned revision and exact file ranges.
book component
archived SLF component
exact boundary
separating conjunction
hstar in Hprop.v
same disjoint finite-map split
semantic triple
triple in Triples.v
book: fault freedom and partial correctness; SLF: omni-big-step total correctness
H-Conseq plus H-Frame
triple_conseq_frame in Triples.v
same consequence–frame shape
allocation, free, load, store
triple_ref, triple_free, triple_get, triple_set in Rules.v
SLF commands return values; book commands update named store variables
𝖼𝗁𝖺𝗂𝗇𝑛
MList and MList_if in Repr.v
same separated head–tail recursion; SLF nodes also carry a data field
The SLF definition of triples and its soundness connection include termination, whereas definition 44.12 asserts fault freedom plus postconditions only for terminating executions. The table is therefore a declaration-by-declaration comparison, not an identification of the two semantic judgments and not a shortcut around theorem 44.11, theorem 44.16. The archived course tree leaves triple_conseq_frame, triple_free’, triple_set, and MList_if as Admitted exercises. Their signatures remain comparison evidence; they are not counted here as checked SLF proofs.
For the command grammar of definition 44.6, locality is theorem 44.11 and Hoare-rule soundness is theorem 44.16. Because that grammar has no parallel command or interleaving reduction, neither theorem states a concurrency result.
★☆☆ Replace both stars in proposition 44.17 by ordinary conjunction. Using the exact points-to semantics of definition 44.3, determine whether the new precondition is satisfiable. Explain why an inexact global points-to predicate would instead require an explicit non-aliasing premise.
★☆☆ Compose proposition 44.21 twice to derive the exact triple for removing two cells. State the smallest admissible input length and the resulting length.
★★☆ If 𝜎,ℎ⊧𝖼𝗁𝖺𝗂𝗇𝑛(𝑥)∗𝖼𝗁𝖺𝗂𝗇𝑚(𝑦), prove that |dom(ℎ)|=𝑛+𝑚, and that the two heads denote distinct locations whenever 𝑛,𝑚>0. Identify the exact use of disjointness.
★★☆ Prove that no valid triple with satisfiable precondition can type the exact sequence 𝖿𝗋𝖾𝖾(𝑥);𝑦:=[𝑥]. Give the semantic fault argument and the failed proof-rule premise. Then explain why inserting 𝑥:=𝖺𝗅𝗅𝗈𝖼(𝑣) before the load establishes a new owned address, rather than restoring a guaranteed old address.
★★☆ In the sublanguage whose only command-visible root is 𝑥, derive a valid triple for 𝑥:=𝖺𝗅𝗅𝗈𝖼(0);𝑥:=𝗇𝗎𝗅𝗅 whose postcondition is 𝗍𝗋𝗎𝖾. Explain why this does not contradict proposition 44.22 and which stronger postcondition would expose the unreachable cell.
★☆☆ Using the archived-source locators in appendix D, compare the statements of H-Frame, H-Alloc, H-Free, H-Load, and H-Store with triple_conseq_frame, triple_ref, triple_free, triple_get, and triple_set. Then unfold MList once and compare it with one unfolding of 𝖼𝗁𝖺𝗂𝗇𝑛+1. Record the triple semantics, return-value convention, and node layout at every mismatch. Explain why these comparisons do not transfer SLF soundness to this chapter’s command language.
★★★Practical project.separation-symbolic-executor Implement the finite store, heap, and command evaluator in Kappa together with the exact footprint predicates needed by the worked examples. Maintain these invariants:
heap union is performed only on disjoint domains;
a missing load, store, or free address reports a fault rather than a default value;
allocation returns a location absent from the current heap; and
exact points-to and chain predicates check footprint size as well as stored values.
The oracle must accept a framed cell update, allocation followed by deallocation, push then pop on an exact two-cell chain, and exact singleton points-to; it must report a fault for load after free and reject an aliased separating conjunction. Mutate missing heap lookup to return 𝗇𝗎𝗅𝗅; the mutant must type-check and audit cleanly but fail the use-after-free oracle. Appendix E records the four acceptance commands and appendix F gives the implementation stages.