Reasoning about Shared Mutable Data Structure

John C. Reynolds Department of Computer Science

Carnegie Mellon University

and

Peter W. O’Hearn Department of Computer Science Queen Mary and Westfield College

January 15, 2001

(corrected January 23, 2001)

Basic Ideas

• Extention of Hoare logic for imperative programs • Store/heap dichotomy

• Heap-manipulation commands (not expressions)

• Independent conjunction ( ∗)

• Unrestricted address arithmetic

• Heap faults

• Nondeterministic allocation

• Inductive definitions over abstract structures

New Commands

⟨comm⟩ ::= ⋯

| ⟨var⟩:= cons(⟨exp⟩, …, ⟨exp⟩) | ⟨var⟩:= [⟨exp⟩] | [⟨exp⟩] := ⟨exp⟩ | dispose ⟨exp⟩

New Assertions

⟨assert⟩ ::= ⋯

| ⟨exp⟩ ↦ ⟨exp⟩ | emptyheap | ⟨assert⟩ ∗ ⟨assert⟩ | ⟨assert⟩ −∗ ⟨assert⟩

Why cons, car, and cdr do not occur in expressions

(x = x)/x → cons(1, 2) is cons(1, 2) = cons(1, 2)

(x = x ∗ y = y)/x → car(z), y → car(z) is (car(z) = car(z)) ∗ (car(z) = car(z))

Stores and Heaps

Atoms ⊆ Z
Locations ⊆ Z
Atoms ∩ Locations = {}
nil ^{∈} Atoms
States = Stores × Heaps
Stores = ⟨var⟩ → Z
Heaps = ⋃_{A⊆^{fin}Locations}(A → Z)
[[−]]_{exp} ^{∈} ⟨exp⟩ → Stores → Z
[[−]]_{boolexp} ^{∈} ⟨boolexp⟩ → Stores → B
[[−]]_{assert} ^{∈} ⟨assert⟩ → States → B

Structural Operational Semantics

An execution (of a command) is a sequence

γ_{0} ⇝ γ_{1} ⇝ ⋯

of configurations γ_{i} related by the transition relation ⇝. A configuration is either:

• nonterminal: A command-state pair.

• terminal: A state or abort. We write:

• γ ⇝^{∗} γ′ iff there is a finite execution from γ to γ′.

• γ ↑ iff there is an infinite execution beginning with γ. Our semantics is total:

• For every nonterminal configuration γ, there is at least one configuration γ′ such that γ ⇝ γ′, i.e., executions do not get stuck.

• Every execution sequence can be extended to a sequence

that is either infinite or ends with a terminal configuration. The transition relation is defined by inference rules.

Transition Rules for the New Commands

• Construction ⟨v := cons(e_{0}, …, e_{n−1}), (s, h)⟩ ⇝ ([ s | v: ℓ], [ h | ℓ: [[e_{0}]]_{exp}s | … | ℓ + n − 1: [[e_{n−1}]]_{exp}s])

where ℓ, …, ℓ + n − 1 ^{∈} Locations − dom h.

• Lookup

When [[e]]_{exp}s ^{∈} dom h:

\overline{⟨v := [e], (s, h)⟩ ⇝ ([ s | v: h([[e]]_{exp}s) ], h)} When [[e]]_{exp}s ∉ dom h:

\overline{⟨v := [e], (s, h)⟩ ⇝ abort}

More Transition Rules

• Mutation When [[e]]_{exp}s ^{∈} dom h:

\overline{⟨[e] := e′, (s, h)⟩ ⇝ (s, [ h | [[e]]_{exp}s: [[e′]]_{exp}s])}

When [[e]]_{exp}s ∉ dom h:

\overline{⟨[e] := e′, (s, h)⟩ ⇝ abort}

• Disposal When [[e]]_{exp}s ^{∈} dom h:

⟨dispose e, (s, h)⟩ ⇝ (s, h⌉(dom h − {[[e]]_{exp}s})) When [[e]]_{exp}s ∉ dom h:

⟨dispose e, (s, h)⟩ ⇝ abort

Semantics of the New Assertions

[[e ↦ e′]]_{assert}(s, h)

iff dom h = {[[e]]_{exp}s} and h([[e]]_{exp}s) = [[e′]]_{exp}s, [[emptyheap]]_{assert}(s, h)

iff dom h = {}, [[p_{0} ∗ p_{1}]]_{assert}(s, h)

iff ∃h_{0}, h_{1}. h_{0} ⊥ h_{1} and h_{0} · h_{1} = h

and [[p_{0}]]_{assert}(s, h_{0}) and [[p_{1}]]_{assert}(s, h_{1}),

[[p_{0} −∗ p_{1}]]_{assert}(s, h)

iff ∀h′. (h′ ⊥ h and [[p_{0}]]_{assert}(s, h′))

implies [[p_{1}]]_{assert}(s, h · h′),

where

h_{0} ⊥ h_{1} iff dom h_{0} ∩ dom h_{1} = {}
dom(h_{0} · h_{1}) = dom h_{0} ∪ dom h_{1}
(h_{0} · h_{1})ℓ = \{ \begin{matrix}h_{0}ℓ when ℓ ^{∈} dom h_{0} \\ h_{1}ℓ when ℓ ^{∈} dom h_{1}. \end{matrix}

Pure Assertions

An assertion is pure if it does not contain ↦ or emptyheap. A pure assertion does not depend upon the heap.

Pure Commands

A command is pure if it does not contain any of the new commands v := cons(e_{0}, …, e_{n−1}) v := [e] [e] := e′ dispose e. A pure command does not depend upon the heap and does not alter the heap.

Some Abbreviations

e ↦ − =^{def} ∃x′. e ↦ x′ where x′ not free in e
e ↪ e′ =^{def} e ↦ e′ ∗ true
e ↦ e_{0}, …, e_{n−1} =^{def} e ↦ e_{0} ∗ ⋯ ∗ e + n − 1 ↦ e_{n−1}
e ↪ e_{0}, …, e_{n−1} =^{def} e ↪ e_{0} ∗ ⋯ ∗ e + n − 1 ↪ e_{n−1}
iff e ↦ e_{0}, …, e_{n−1} ∗ true

An Example of ∗

[[p_{0} ∗ p_{1}]]_{assert}(s, h)

iff ∃h_{0}, h_{1}. h_{0} ⊥ h_{1} and h_{0} · h_{1} = h and [[p_{0}]]_{assert}(s, h_{0}) and [[p_{1}]]_{assert}(s, h_{1})

x ↦ 3, y ∗ y ↦ 4, x x ↪ 3, y ∗ y ↪ 4, x

[figure: 3; 4; x; y]

\begin{matrix}x ↦ 3, y \\ x ↪ 3, y \end{matrix}  [figure: 3; x; y]

\begin{matrix}y ↦ 4, x \\ y ↪ 4, x \end{matrix}  [figure: 4; x; y]

More Examples of ∗

Suppose s x and s y are distinct locations, so that

h_{1} = {⟨s x, ⟨1⟩⟩} and h_{2} = {⟨s y, ⟨2⟩⟩}. are heaps with disjoint domains. Then

If P is:  then [[P]](s, h) is:
x ↦ 1  h = h_{1}
y ↦ 2  h = h_{2}
x ↦ 1 ∗ y ↦ 2  h = h_{1} · h_{2}
x ↦ 1 ∗ x ↦ 1  false
x ↦ 1 ∨ y ↦ 2  h = h_{1} or h = h_{2}
x ↦ 1 ∗ (x ↦ 1 ∨ y ↦ 2)  h = h_{1} · h_{2}
(x ↦ 1 ∨ y ↦ 2) ∗ (x ↦ 1 ∨ y ↦ 2) h = h_{1} · h_{2}
x ↦ 1 ∗ y ↦ 2 ∗ (x ↦ 1 ∨ y ↦ 2)  false
x ↦ 1 ∗ true  h_{1} ⊆ h
x ↦ 1 ∗ ¬ x ↦ 1  h_{1} ⊆ h

Rules and Axiom Schemata for ∗ and −∗

p_{1} ∗ p_{2} ⇔ p_{2} ∗ p_{1}
(p_{1} ∗ p_{2}) ∗ p_{3} ⇔ p_{1} ∗ (p_{2} ∗ p_{3})
p ∗ emptyheap ⇔ p
(p_{1} ∨ p_{2}) ∗ q ⇔ (p_{1} ∗ q) ∨ (p_{2} ∗ q)
(p_{1} ∧ p_{2}) ∗ q ⇒ (p_{1} ∗ q) ∧ (p_{2} ∗ q)
(∃x. p_{1}) ∗ p_{2} ⇔ ∃x. (p_{1} ∗ p_{2}) when x not free in p_{2}
(∀x. p_{1}) ∗ p_{2} ⇒ ∀x. (p_{1} ∗ p_{2}) when x not free in p_{2}.

\frac{p_{1} ⇒ p_{2} q_{1} ⇒ q_{2}}{p_{1} ∗ q_{1} ⇒ p_{2} ∗ q_{2}.}

\frac{p_{1} ∗ p_{2} ⇒ p_{3}}{p_{1} ⇒ (p_{2} −∗ p_{3})}  \frac{p_{1} ⇒ (p_{2} −∗ p_{3})}{p_{1} ∗ p_{2} ⇒ p_{3}}

Axiom Schemata for ↦

x ↦ e ∧ x′ ↦ e′ ⇔ x ↦ e ∧ x = x′ ∧ e = e′
(x ↦ e ∗ true) ∧ emptyheap ⇔ false
x ↦ e ∗ x′ ↦ e′ ⇒ x ≠ x′.

Axiom Schemata for Purity

p_{1} ∧ p_{2} ⇒ p_{1} ∗ p_{2} when p_{1} or p_{2} is pure
p_{1} ∗ p_{2} ⇒ p_{1} ∧ p_{2} when p_{1} and p_{2} are pure
(p ∧ q) ∗ r ⇔ (p ∗ r) ∧ q when q is pure
(p_{1} −∗ p_{2}) ⇒ (p_{1} ⇒ p_{2}) when p_{1} is pure
(p_{1} ⇒ p_{2}) ⇒ (p_{1} −∗ p_{2}) when p_{1} and p_{2} are pure

In addition, the model validates all of the laws of classical logic for ¬, ⇒, ∧ and ∨. It uses the boolean algebra structure of the powerset of Heaps, which amounts to pointwise interpretations for each classical connective.

Two Unsound Axiom Schemata

p ⇏ p ∗ p  (Contraction)
e.g. p: x ↦ 1
p ∗ q ⇏ p  (Weakening)
e.g. p: x ↦ 1
q: y ↦ 2

An Example of −∗

[[p_{0} −∗ p]]_{assert} iff ∀h′. (h′ ⊥ h and [[p_{0}]]_{assert}(s, h′))

implies [[p_{1}]]_{assert}(s, h · h′)

If:

P  [figure: 7; x; 5; Rest; of; Heap]

then:

x ↦ 7, 5 −∗ P  [figure: x; All; of; Heap]

and:

x ↦ 3, 5 ∗ (x ↦ 7, 5 −∗ P) [figure: 3; x; 5; Rest; of; Heap]

Specifications

[[−]]_{spec} ^{∈} ⟨spec⟩ → B.

Partial correctness:

[[{p} c {q}]]_{spec} iff ∀σ ^{∈} States. [[p]]_{assert}σ implies

¬ c, σ ⇝^{∗} abort

and (∀σ′. c, σ ⇝^{∗} σ′ implies [[q]]_{assert}σ′)

Total correctness:

[[[ p] c [ q ]]]_{spec} iff ∀σ ^{∈} States. [[p]]_{assert}σ implies

¬ c, σ ⇝^{∗} abort

and ¬ c, σ ↑

and (∀σ′. c, σ ⇝^{∗} σ′ implies [[q]]_{assert}σ′).

• Specifications are implicitly quantified over both stores and heaps — and over all executions.

• An execution giving a memory fault falsifies a specification.

An Inference Rule for Mutation

{p ∗ (e ↦ −)} [e] := e′ {p ∗ (e ↦ e′)}

An Inference Rule for Construction

{p} v := cons(e_{0}, …, e_{n−1}) {p ∗ (v ↦ e_{0}, …, e_{n−1})}

where v is not free in e_{0}, …, e_{n−1}, or p.

A Stronger Rule

{p} v := cons(e_{0}, …, e_{n−1}) {∃v′. p′ ∗ (v ↦ e′_{0}, …, e′_{n−1})}

where • v′ is distinct from v and not free in e_{0}, …, e_{n−1}, or p,

• p′ is the substitution p/v → v′,

• each e′_{i} is the subsitution e_{i}/v → v′.

Violating Record Boundaries

{p}

x := cons(1, 2)

⋮  (no assignment to x)

[x + 2] := 3

{q}

cannot hold, since there will be some execution in which s x+2 ∉ dom h before the execution of [x + 2] := 3. If one tries to prove such a specification:

{p} x := cons(1, 2)

{∃x′. (p/x → x′) ∗ x ↦ 1, 2} ≡ {∃x′. (p/x → x′)
∗ x ↦ 1 ∗ x + 1 ↦ 2}
⋮ ⋮ (no implication)
{q ∗ (x + 2 ↦ −)}  ≡ {q ∗ (∃y. x + 2 ↦ y)}

[x + 2] := 3 {q ∗ (x + 2 ↦ 3)}

An Inference Rule for Lookup

{∃v′. p′ ∧ e ↪ v′}
v := [e]
{p}

where v′ does not occur free in p or e, and p′ is p/v → v′.

Disposal

{p ∗ (e ↦ −)}
dispose e
{p}

Frame Introduction (Generalized Constancy)

\frac{\{p\} c \{q\}}{\{p ∗ r\} c \{q ∗ r\}}

when no variable occurs both free in r and free on the left of an assignment command in c.

For all of the new inference rules, there are similar rules for total correctness.

An Inductive Definition: Singly-Linked Lists

list α (i, j):  [figure: α_{1}; i; ⋯; ^{j α_{n}}]

Definition

list ϵ (i, j) =^{def} emptyheap ∧ i = j
list a·α (i, k) =^{def} ∃j. i ↦ a, j ∗ list α (j, k)

Properties

list a (i, j) ⇔ i ↦ a, j
list α·β (i, k) ⇔ ∃j. list α (i, j) ∗ list β (j, k)
list α·b (i, k) ⇔ ∃j. list α (i, j) ∗ j ↦ b, k

Cycles

When

ai^{}i

we have • list ϵ (i, i) holds for the empty heap.

• list a (i, i) holds for the two-element heap pictured above. But because of the ∗ in

list a·α (i, k) =^{def} ∃j. i ↦ a, j ∗ list α (j, k),

list a·a (i, i), list a·a·a (i, i), … do not hold.

Emptyness Conditions

list α (i, j) ⇒ ( \begin{matrix}& (i = nil & ⇒ & (α = ϵ ∧ j = nil)) \\ ∧ & (i ≠ j & ⇒ & α ≠ ϵ). \end{matrix} )

Inserting a List Element

• At the beginning:

{list α (i, j)} k := cons(a, i); {list α (i, j) ∗ k ↦ a, i} {∃i. k ↦ a, i ∗ list α (i, j)} {list a·α (k, j)} i := k {list a·α (i, j)}

• At the end of a nonempty segment:

{list α (i, j) ∗ j ↦ a, k} l := cons(b, k) ; {list α (i, j) ∗ j ↦ a, k ∗ l ↦ b, k} {list α (i, j) ∗ j ↦ a ∗ j + 1 ↦ k ∗ l ↦ b, k} {list α (i, j) ∗ j ↦ a ∗ j + 1 ↦ − ∗ l ↦ b, k} [j + 1] := l {list α (i, j) ∗ j ↦ a ∗ j + 1 ↦ l ∗ l ↦ b, k} {list α (i, j) ∗ j ↦ a, l ∗ l ↦ b, k} {list α·a (i, l) ∗ l ↦ b, k} {list α·a·b (i, k)}

Deleting a List Element

• At the beginning:

{list a·α (i, k)} {∃j. i ↦ a, j ∗ list α (j, k)}

⋮ {∃j. (i ↦ a, j ∗ list α (j, k)) ∧ i + 1 ↪ j} j := [i + 1] ; {i ↦ a, j ∗ list α (j, k)} {i ↦ a ∗ i + 1 ↦ j ∗ list α (j, k)} dispose i ; {i + 1 ↦ j ∗ list α (j, k)} dispose i + 1 ; {list α (j, k)} i := j {list α (i, k)}

• At the end of a nonempty segment: {list α (i, j) ∗ j ↦ a, k ∗ k ↦ b, l} [j + 1] := l ; {list α (i, j) ∗ j ↦ a, l ∗ k ↦ b, l} dispose k ; dispose k + 1 {list α (i, j) ∗ j ↦ a, l} {list α·a (i, l)}

Reversing a List

{list γ (i, nil)} {list γ (i, nil) ∗ emptyheap} j := nil ; {list γ (i, nil) ∗ (emptyheap ∧ j = nil)} {list γ (i, nil) ∗ list ϵ (j, nil)} {∃α, β. (list α (i, nil) ∗ list β (j, nil)) ∧ γ^{†} = α^{†}·β} while i ≠ nil do ({∃a, α, β. (list a·α (i, nil) ∗ list β (j, nil)) ∧ γ^{†} = (a·α)^{†}·β} {∃a, α, β, k. (i ↦ a, k ∗ list α (k, nil) ∗ list β (j, nil))

∧ γ^{†} = (a·α)^{†}·β} k := [i + 1] ; {∃a, α, β. (i ↦ a, k ∗ list α (k, nil) ∗ list β (j, nil))

∧ γ^{†} = (a·α)^{†}·β} [i + 1] := j ; {∃a, α, β. (i ↦ a, j ∗ list α (k, nil) ∗ list β (j, nil))

∧ γ^{†} = (a·α)^{†}·β} {∃a, α, β. (list α (k, nil) ∗ list a·β (i, nil)) ∧ γ^{†} = α^{†}·a·β} {∃α, β. (list α (k, nil) ∗ list β (i, nil)) ∧ γ^{†} = α^{†}·β} j := i ; i := k {∃α, β. (list α (i, nil) ∗ list β (j, nil)) ∧ γ^{†} = α^{†}·β})

{∃α, β. list β (j, nil) ∧ γ^{†} = α^{†}·β ∧ α = ϵ} {list γ^{†} (j, nil)}

An Inductive Definition: Doubly-Linked Lists

dlist α (i, i′, j, j′):  [figure: i′; α_{1}; i; ⋯; ⋯; j; α_{n}; j′]

Definition

dlist ϵ (i, i′, j, j′) =^{def} emptyheap ∧ i = j ∧ i′ = j′
dlist a·α (i, i′, k, k′) =^{def} ∃j. i ↦ a, j, i′ ∗ dlist α (j, i, k, k′).

Properties

dlist a (i, i′, j, j′) ⇔ i ↦ a, j, i′ ∧ i = j′
dlist α·β (i, i′, k, k′) ⇔ ∃j, j′. dlist α (i, i′, j, j′) ∗ dlist β (j, j′, k, k′)
dlist α·b (i, i′, k, k′) ⇔ ∃j′. dlist α (i, i′, k′, j′) ∗ k′ ↦ b, k, j′.

Emptyness Conditions

dlist α (i, i′, j, j′) ⇒ ( \begin{matrix}& (i = nil & ⇒ & (α = ϵ ∧ j = nil ∧ i′ = j′)) \\ ∧ & (j′ = nil & ⇒ & (α = ϵ ∧ i′ = nil ∧ i = j)) \\ ∧ & (i ≠ j & ⇒ & α ≠ ϵ) \\ ∧ & (i′ ≠ j′ & ⇒ & α ≠ ϵ) \end{matrix} )

Deleting an Element from a Doubly-Linked List

[figure: nil; α_{1}; i; ⋯; ⋯; α_{m}; (j); b; k; β_{1}; (l); ⋯; ⋯; nil; β_{n}; m]

{∃j, l. dlist α (i, nil, k, j) ∗ k ↦ b, l, j ∗ dlist β (l, k, nil, m)} l := [k + 1] ; j := [k + 2] ; {dlist α (i, nil, k, j) ∗ k ↦ b, l, j ∗ dlist β (l, k, nil, m)} dispose k ; dispose k + 1 ; dispose k + 2 ; {dlist α (i, nil, k, j) ∗ dlist β (l, k, nil, m)} if j = nil then

{dlist β (l, k, nil, m) ∧ i = k ∧ nil = j ∧ α = ϵ} i := l {dlist β (l, k, nil, m) ∧ i = l ∧ nil = j ∧ α = ϵ}

else

{∃α′, a, n. (dlist α′ (i, nil, j, n) ∗ j ↦ a, k, n

∗ dlist β (l, k, nil, m)) ∧ α = α′·a} [j + 1] := l ; {∃α′, a, n. (dlist α′ (i, nil, j, n) ∗ j ↦ a, l, n

∗ dlist β (l, k, nil, m)) ∧ α = α′·a} {dlist α (i, nil, l, j) ∗ dlist β (l, k, nil, m)}

⋮

Deleting from a Doubly-Linked List (continued)

⋮ {dlist α (i, nil, l, j) ∗ dlist β (l, k, nil, m)} if l = nil then

{dlist α (i, nil, l, j) ∧ l = nil ∧ k = m ∧ β = ϵ} m := j {dlist α (i, nil, l, j) ∧ l = nil ∧ j = m ∧ β = ϵ}

else

{∃a, β′, n. (dlist α (i, nil, l, j) ∗ l ↦ a, n, k

∗ dlist β′ (n, l, nil, m)) ∧ β = a·β′} [l + 2] := j {∃a, β′, n. (dlist α (i, nil, l, j) ∗ l ↦ a, n, j

∗ dlist β′ (n, l, nil, m)) ∧ β = a·β′} {dlist α (i, nil, l, j) ∗ dlist β (l, j, nil, m)} {dlist α·β (i, nil, nil, m)}

Trees (Binary)

τ ^{∈} Trees iff

τ ^{∈} Atoms
or τ = (τ_{1}, τ_{2}) where τ_{1}, τ_{2} ^{∈} Trees

e.g.

((a, (b, c)), (d, e)) =  [figure: ·; ·; ·; a; ·; d; e; b; c]

Tree Segments

τ ^{∈} Trees(n) iff

τ = k̂ where 1 ≤ k ≤ n
τ ^{∈} Atoms
or τ = (τ_{1}, τ_{2}) where τ_{1}, τ_{2} ^{∈} Trees(n)

e.g.

((ˆ1, (b, ˆ2)), (d, ˆ1)) =  [figure: ·; ·; ·; ˆ1; ·; d; ˆ1; b; ˆ2]

Tree Representation (without sharing)

For τ ^{∈} Trees(n), we define the assertion

tree τ (i : j_{1}, … j_{n})

by structural induction:

tree k̂ (i : j_{1}, … j_{n}) iff emptyheap ∧ i = j_{k}
tree a (i : j_{1}, … j_{n}) iff emptyheap ∧ i = a
tree (τ_{1}, τ_{2}) (i : j_{1}, … j_{n}) iff ∃i_{1}, i_{2}. i ↦ i_{1}, i_{2}

∗ tree τ_{1} (i_{1} : j_{1}, … j_{n}) ∗ tree τ_{2} (i_{2} : j_{1}, … j_{n})

Tree Representation (with sharing)

For τ ^{∈} Trees(n), we define

stree τ (i : j_{1}, … j_{n})

by:

stree k̂ (i : j_{1}, … j_{n}) iff i = j_{k}
stree a (i : j_{1}, … j_{n}) iff i = a
stree (τ_{1}, τ_{2}) (i : j_{1}, … j_{n}) iff ∃i_{1}, i_{2}. i ↦ i_{1}, i_{2}
∗ (stree τ_{1} (i_{1} : j_{1}, … j_{n}) ∧ stree τ_{2} (i_{2} : j_{1}, … j_{n}))

A Problem

Suppose we wish to prove that a recursively defined procedure copytree satisfies

{stree τ(i :)} copytree(i, j) {stree τ(i :) ∗ tree τ(j :)}

Then, we must use this specification as a hypothesis in proving that the recursive calls in the procedure body satisfy:

{stree τ_{1}(i_{1} :) ∧ stree τ_{2}(i_{2} :)}

copytree(i_{1}, j_{1})

{(stree τ_{1}(i_{1} :) ∧ stree τ_{2}(i_{2} :)) ∗ tree τ_{1}(j_{1} :)}

copytree(i_{2}, j_{2})

{(stree τ_{1}(i_{1} :) ∧ stree τ_{2}(i_{2} :)) ∗ tree τ_{1}(j_{1} :) ∗ tree τ_{2}(j_{2} :)} But the hypothesis is not strong enough to imply this.

Possible solutions:

• Introduce passivity.

• Introduce auxiliary variables denoting assertions: {stree τ(i :) ∧ p} copytree(i, j) {(stree τ(i :) ∧ p) ∗ tree τ(j :)}

• Introduce auxiliary variables denoting heaps: this(h).

Iterated Independent Conjunction

m > n ⇒ (⨀_{i=m}^{n} p(i) ⇔ emptyheap)
m = n ⇒ (⨀_{i=m}^{n} p(i) ⇔ p(m))
k ≤ m ≤ n + 1 ⇒ (⨀_{i=k}^{n} p(i) ⇔ (⨀_{i=k}^{m−1} p(i) ∗ ⨀_{i=m}^{n} p(i)))

An Inference Rule for Array Allocation

{p} v := allocate e {p ∗ ⨀_{i=v}^{v+e−1} i ↦ −}

where v does not occur free in p or e.

Future Directions

• Directed graphs

• Dynamic logic and refinement calculi

• Assertions versus types

• Garbage collection

{emptyheap} x := cons_{2}(1, 2) ; {x → 1, 2} x := 3 {(∃x. x → 1, 2) ∧ x = 3}

• Concurrency

References

[1] Rodney M. Burstall. Some techniques for proving correctness of programs which alter data structures. In Bernard Meltzer and Donald Michie, editors, Machine Intelligence 7, pages 23–50. Edinburgh University Press, Edinburgh, Scotland, 1972.

[2] Peter W. O’Hearn and David J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215–244, June 1999.

[3] John C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science, pages 303–321, Houndsmill, Hampshire, 2000. Palgrave.

[4] Samin Ishtiaq and Peter W. O’Hearn. BI as an assertion language for mutable data structures. In Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 14–26, New York, 2001. ACM.