Lectures on Reasoning about Shared Mutable Data Structure

Part 1

John C. Reynolds

Department of Computer Science

Carnegie Mellon University

and

BRICS, Department of Computer Science University of Aarhus

Joint work with

Peter W. O’Hearn and Hongseok Yang

June 18, 2001, corrected June 29

The topic of these lectures is an extension of Hoare logic [1, 2] to the specification and proof of programs in which data structures can contain several pointers to the same location, whose contents can be modified by the program. The central idea, of an “independent conjunction” p ∗ q that asserts that p and q hold for separate parts of the data structure, is implicit in early work by Burstall [3]. It was explicitly described by Reynolds in lectures in the fall of 1999; then an intuitionistic logic based on this idea was discovered independently by Reynolds [20] and by Ishtiaq and O’Hearn [21]. Ishtiaq and O’Hearn realized that this logic was a special case of a bunched implication logic [18], and also introduced an “independent implication” operation. In addition, Ishtiaq and O’Hearn devised a classical version of the logic that is more expressive than the intuitionistic version. (In particular, it can express storage deallocation.) Recently, Reynolds extended the classical version by adding pointer arithmetic [23]; it is this extension that will be used in these lectures. We will also make use of O’Hearn’s “frame rule” [26, 27], which permits local reasoning about components of programs. Other recent relevant papers include work by Calcagno on the treatment of garbage collection in the intuitionistic logic [24], by Yang on a proof of the Schorr-Waite Algorithm [25], and by Walker and Morrisett on a type system with goals that are similar to our logics [22]. The research of my own that is described in these lectures was supported by National Science Foundation Grant CCR–9804014.

References

[1] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580 and 583, October 1969.

[2] C. A. R. Hoare. Proof of a program: FIND. Communications of the ACM, 14(1):39–45, January 1971.

[3] 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.

[4] T. Kowaltowski. Correctness of programs manipulating data structures. Memorandum ERL-M404, University of California, Berkeley, California, September 1973.

[5] Stephen A. Cook and Derek C. Oppen. An assertion language for data structures. In Conference Record of the Second ACM Symposium on Principles of Programming Languages, pages 160–166, New York, 1975. ACM.

[6] Derek C. Oppen and Stephen A. Cook. Proving assertions about programs that manipulate data structures. In Proceedings of Seventh Annual ACM Symposium on Theory of Computing, pages 107–116, New York, 1975. ACM.

[7] Joseph M. Morris. A general axiom of assignment; assignment and linked data structures; a proof of the Schorr-Waite algorithm. In Manfried Broy and Gunther Schmidt, editors, Theoretical Foundations of Programming Methodology, pages 25–51. D. Reidel, Dordrecht, Holland, 1982.

[8] Ian A. Mason. The Semantics of Destructive Lisp. CSLI Lecture Notes Number 5. Center for the Study of Language and Information, Menlo Park, CA, 1986.

[9] Ian A. Mason. Verification of programs that destructively manipulate data. Science of Computer Programming, 10(2):177–210, April 1988.

[10] Ian A. Mason and Carolyn Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1(3):287–327, July 1991.

[11] Furio Honsell, Ian A. Mason, Scott Smith, and Carolyn Talcott. A variable typed logic of effects. Information and Computation, 119(1):55–90, May 15, 1995.

[12] Ian A. Mason. A first order logic of effects. Theoretical Computer Science, 185(2):277–318, October 20, 1997.

[13] Ian D. B. Stark. Names and Higher-Order Functions. Ph. D. dissertation, University of Cambridge, Cambridge, England, December 1994.

[14] Ian D. B. Stark. Categorical models for local names. Lisp and Symbolic Computation, 9(1):77–107, February 1996.

[15] Ian D. B. Stark. Names, equations, relations: Practical ways to reason about new. Fundamenta Informaticae, 33:369–396, 1998.

[16] Andrew M. Pitts and Ian D. B. Stark. Operational reasoning for functions with local state. In Andrew D. Gordon and Andrew M. Pitts, editors, Higher Order Operational Techniques in Semantics, pages 227–273. Cambridge University Press, 1998.

[17] John C. Reynolds. Theories of Programming Languages. Cambridge University Press, Cambridge, England, 1998.

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

[19] Cristiano Calcagno, Samin Ishtiaq, and Peter W. O’Hearn. Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic. unpublished, 2000.

[20] John C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Jim Davies, Bill Roscoe, and Jim Woodcock, editors, Millennial Perspectives in Computer Science, pages 303–321, Houndsmill, Hampshire, 2000. Palgrave.

[21] 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.

[22] David Walker and Greg Morrisett. Alias types for recursive data structures. In Preliminary Proceedings of the Third Workshop on Types in Compilation (TIC 2000). School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, 2000. Report CMU–CS–00–161.

[23] John C. Reynolds and Peter W. O’Hearn. Reasoning about shared mutable data structure (abstract of invited lecture). In Fritz Henglein, John Hughes, Henning Makholm, and Henning Niss, editors, SPACE 2001: Informal Proceedings of Workshop on Semantics, Program Analysis and Computing Environments for Memory Management, page 7. IT University of Copenhagen, 2001. The slides for this lecture are available at ftp://ftp.cs.cmu.edu/user/jcr/spacetalk.ps.gz.

[24] Cristiano Calcagno. Program logics in the presence of garbage collection (abstract). In Fritz Henglein, John Hughes, Henning Makholm, and Henning Niss, editors, SPACE 2001: Informal Proceedings of Workshop on Semantics, Program Analysis and Computing Environments for Memory Management, page 11. IT University of Copenhagen, 2001.

[25] Hongseok Yang. An example of local reasoning in BI pointer logic: The Schorr-Waite graph marking algorithm. In Fritz Henglein, John Hughes, Henning Makholm, and Henning Niss, editors, SPACE 2001: Informal Proceedings of Workshop on Semantics, Program Analysis and Computing Environments for Memory Management, pages 41–68. IT University of Copenhagen, 2001.

[26] Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures.

In Proceedings of 15th Annual Conference of the European Association for Computer Science Logic: CSL 2001, Lecture Notes in Computer Science, Berlin, 2001. Springer-Verlag. To appear.

[27] Hongseok Yang. Local Reasoning for Stateful Programs. Ph. D. dissertation, University of Illinois, Urbana-Champaign, Illinois, 2001. (expected).

Abstract Syntax of the Programming Language

⟨exp⟩ ::= 0 | 1 | 2 | ⋯ | ⟨var⟩ | − ⟨exp⟩ | ⟨exp⟩ + ⟨exp⟩ | ⟨exp⟩ − ⟨exp⟩ | ⟨exp⟩ × ⟨exp⟩ | ⋯

⟨boolexp⟩ ::= true | false | ⟨exp⟩ = ⟨exp⟩ | ⟨exp⟩ ≠ ⟨exp⟩ | ⋯ | ¬ ⟨boolexp⟩ | ⟨boolexp⟩ ∧ ⟨boolexp⟩ | ⟨boolexp⟩ ∨ ⟨boolexp⟩ | ⟨boolexp⟩ ⇒ ⟨boolexp⟩ | ⟨boolexp⟩ ⇔ ⟨boolexp⟩

⟨comm⟩ ::= ⟨var⟩:= ⟨exp⟩ | skip | ⟨comm⟩; ⟨comm⟩ | if ⟨boolexp⟩ then ⟨comm⟩ else ⟨comm⟩ | while ⟨boolexp⟩ do ⟨comm⟩ | newvar ⟨var⟩ in ⟨comm⟩ | ⟨var⟩:= cons(⟨exp⟩, …, ⟨exp⟩) | ⟨var⟩:= [⟨exp⟩] | [⟨exp⟩] := ⟨exp⟩ | dispose ⟨exp⟩

Stores and Heaps

Atoms ⊆ Z
Locations ⊆ Z
Atoms ∩ Locations = {}
nil ^{∈} Atoms
States = Stores × Heaps
Stores = ⟨var⟩ → Z
Heaps = ⋃_{A⊆^{fin}Locations}(A → Z)

Eventually, stores will map

ordinary variables into Z
sequence variables into sequences
tree variables into trees
assertion variables into Heaps → B
⋮

Semantic Equations

[[−]]_{exp} ^{∈} ⟨exp⟩ → Stores → Z
[[−]]_{boolexp} ^{∈} ⟨boolexp⟩ → Stores → B
[[−]]_{assert} ^{∈} ⟨assert⟩ → Stores → Heaps → B

The Semantics of Expressions

[[−]]_{exp} ^{∈} ⟨exp⟩ → Stores → Z.
[[0]]_{exp}s = 0 (and similarly for 1, 2, …),
[[v]]_{exp}s = sv,
[[ − e]]_{exp}s = − [[e]]_{exp}s,
[[e_{0} + e_{1}]]_{exp}s = [[e_{0}]]_{exp}s + [[e_{1}]]_{exp}s

(and similarly for −, ×, …).

[[−]]_{boolexp} ^{∈} ⟨boolexp⟩ → Stores → B.
[[true]]_{boolexp}s = true,
[[false]]_{boolexp}s = false,
[[e_{0} = e_{1}]]_{boolexp}s = ([[e_{0}]]_{exp}s = [[e_{1}]]_{exp}s)

(and similarly for ≠, …),

[[ ¬ b]]_{boolexp}s = ¬[[b]]_{boolexp}s,
[[b_{0} ∧ b_{1}]]_{boolexp}s = [[b_{0}]]_{boolexp}s ∧ [[b_{1}]]_{boolexp}s

(and similarly for ∨, ⇒, ⇔).

An Example

[[x + y = x]]_{boolexp}s = ([[x + y]]_{exp}s = [[x]]_{exp}s)
= ([[x]]_{exp}s + [[y]]_{exp}s = [[x]]_{exp}s)
= (s x + s y = s x)
= (s y = 0).

Substitution

We write

p/v_{1} → e_{1}, …, v_{n} → e_{n}

to denote the phrase obtained from p by simulataneously substituting each expression e_{i} for the variable v_{i}, with renaming of bound variables to avoid capture.

Proposition 1 Let δ abbreviate the substitution

v_{1} → e_{1}, …, v_{n} → e_{n},

and for any store s, let

ŝ = [ v_{1}: [[e_{1}]]_{exp}s | … | v_{n}: [[e_{n}]]_{exp}s].

If e is an expression (or boolean expression) whose free variables belong to {v_{1}, …, v_{n}}, then

[[e/δ]]_{exp}s = [[e]]_{exp}ŝ.

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. For example:

⟨x := x + 1 ; y := y + x ; x := x + 1, ([ x: 3 | y: 7 ], [ ])⟩ ⇝

⟨y := y + x ; x := x + 1, ([ x: 4 | y: 7 ], [ ])⟩ ⇝
⟨x := x + 1, ([ x: 4 | y: 11 ], [ ])⟩ ⇝
([ x: 5 | y: 11 ], [ ]).

⟨x := cons(1, 2) ; y := [x] ; [x + 1] := 3, ([ x: 3 | y: 4 ], [ ])⟩ ⇝

⟨y := [x] ; [x + 1] := 3, ([ x: 37 | y: 4 ], [ 37: 1 | 38: 2 ])⟩ ⇝

⟨[x + 1] := 3, ([ x: 37 | y: 1 ], [ 37: 1 | 38: 2 ])⟩ ⇝
([ x: 37 | y: 1 ], [ 37: 1 | 38: 3 ]).

⟨x := cons(1, 2) ; y := [x + 2] ; [x + 1] := 3, ([ x: 3 | y: 4 ], [ ])⟩ ⇝

⟨y := [x + 2] ; [x + 1] := 3, ([ x: 37 | y: 4 ], [ 37: 1 | 38: 2 ])⟩ ⇝ abort.

Structural Operational Semantics: Notation

We write:

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

• γ ↑ iff there is an infinite execution beginning with γ. Proposition 2 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 called transition rules.

Transition Rules for the Simple Imperative Language

• Assignment

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

• Sequencing

\frac{⟨c_{0}, (s, h)⟩ ⇝ (s′, h′)}{⟨c_{0} ; c_{1}, (s, h)⟩ ⇝ ⟨c_{1}, (s′, h′)⟩}

\frac{⟨c_{0}, (s, h)⟩ ⇝ ⟨c′_{0}, (s′, h′)⟩}{⟨c_{0} ; c_{1}, (s, h)⟩ ⇝ ⟨c′_{0} ; c_{1}, (s′, h′)⟩}

\frac{⟨c_{0}, (s, h)⟩ ⇝ abort}{⟨c_{0} ; c_{1}, (s, h)⟩ ⇝ abort}

For example:

⟨x := x + 1, ([ x: 3 | y: 7 ], [ ])⟩ ⇝ ([ x: 4 | y: 7 ], [ ])
⟨x := x + 1 ; y := y + x, ([ x: 3 | y: 7 ], [ ])⟩ ⇝
⟨y := y + x, ([ x: 4 | y: 7 ], [ ])⟩

⟨(x := x + 1 ; y := y + x) ; x := x + 1, ([ x: 3 | y: 7 ], [ ])⟩ ⇝ ⟨y := y + x ; x := x + 1, ([ x: 4 | y: 7 ], [ ])⟩

Conditional, while, and newvar Commands

• Conditional

When [[b]]_{boolexp}s = true:

⟨if b then c_{0} else c_{1}, (s, h)⟩ ⇝ ⟨c_{0}, (s, h)⟩ When [[b]]_{boolexp}s = false:

⟨if b then c_{0} else c_{1}, (s, h)⟩ ⇝ ⟨c_{1}, (s, h)⟩

• while

When [[b]]_{boolexp}s = true:

⟨while b do c, (s, h)⟩ ⇝ ⟨c; while b do c, (s, h)⟩ When [[b]]_{boolexp}s = false:

\overline{⟨while b do c, (s, h)⟩ ⇝ (s, h)}

• newvar

⟨newvar v in c, (s, h)⟩ ⇝ ⟨c; v := n, ([ s | v: m], h)⟩ where m ^{∈} Z and n = s v.

(See [17, Section 6.2, pp. 128–130] for a discussion of the limitations of this transition rule for newvar.)

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 New Commands

• 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

Free and Free Assigned Variables

FV(c) = “The variables occurring free in c”
FA(c) = “The free variables assigned by c”
FA(v := e) = {v}
FA(v := cons(e_{0}, …, e_{n−1})) = {v}
FA(v := [e]) = {v}
FA(skip) = {}
FA([e] := e′) = {}
FA(dispose e) = {}
FA(c_{0} ; c_{1}) = FA(c_{0}) ∪ FA(c_{1})
FA(if b then c_{0} else c_{1}) = FA(c_{0}) ∪ FA(c_{1})
FA(while b do c) = FA(c)
FA(newvar v in c) = FA(c) − {v}

Proposition 3 If ⟨c, (s, h)⟩ ⇝^{∗} (s′, h′) and v ∉ FA(c), then s′v = s v.

Substitution

Proposition 4 Let c be a command such that FV(c) ⊆ {v_{1}, …, v_{n}}, let δ be a substitution

v_{1} → e_{1}, …, v_{n} → e_{n}

such that, when v_{i} ^{∈} FA(c), e_{i} is a variable that does not occur in any other e_{j}. For any store s, let

ŝ = [ v_{1}: [[e_{1}]]_{exp}s | … | v_{n}: [[e_{n}]]_{exp}s].

Then • If ⟨c/δ, (s, h)⟩ ⇝ (s′, h′), then ⟨c, (ŝ, h)⟩ ⇝ (ŝ′.h′).

• If ⟨c/δ, (s, h)⟩ ⇝ ⟨c̃, (s′, h′)⟩, then there is a command c′ such that ⟨c, (ŝ, h)⟩ ⇝ ⟨c′, (ŝ′.h′)⟩ and c̃ = c′/δ.

• If ⟨c/δ, (s, h)⟩ ⇝ abort, then ⟨c, (ŝ, h)⟩ ⇝ abort. and therefore

• If ⟨c/δ, (s, h)⟩ ⇝^{∗} (s′, h′), then ⟨c, (ŝ, h)⟩ ⇝^{∗} (ŝ′.h′).

• If ⟨c/δ, (s, h)⟩ ⇝^{∗} abort, then ⟨c, (ŝ, h)⟩ ⇝^{∗} abort.

• If ⟨c/δ, (s, h)⟩ ↑, then ⟨c, (ŝ, h)⟩ ↑.

Splitting the Heap

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}

Proposition 5 Suppose h = h_{0} · h_{1}, where h_{0} ⊥ h_{1}. Then • If ⟨c, (s, h)⟩ ⇝ abort, then ⟨c, (s, h_{0})⟩ ⇝ abort.

• If ⟨c, (s, h)⟩ ⇝ ⟨c′, (s′, h′)⟩ then ⟨c, (s, h_{0})⟩ ⇝ abort or ⟨c, (s, h_{0})⟩ ⇝ ⟨c′, (s′, h′_{0})⟩, where h′_{0} ⊥ h_{1} and h′ = h′_{0} · h_{1}.

• If ⟨c, (s, h)⟩ ⇝ (s′, h′) then ⟨c, (s, h_{0})⟩ ⇝ abort or

⟨c, (s, h_{0})⟩ ⇝ (s′, h′_{0}), where h′_{0} ⊥ h_{1} and h′ = h′_{0} · h_{1}. and therefore

• If ⟨c, (s, h)⟩ ⇝^{∗} abort, then ⟨c, (s, h_{0})⟩ ⇝^{∗} abort.

• If ⟨c, (s, h)⟩ ⇝^{∗} (s′, h′) then ⟨c, (s, h_{0})⟩ ⇝^{∗} abort or ⟨c, (s, h_{0})⟩ ⇝^{∗} (s′, h′_{0}), where h′_{0} ⊥ h_{1} and h′ = h′_{0} · h_{1}.

• If ⟨c, (s, h)⟩ ↑ then ⟨c, (s, h_{0})⟩ ⇝^{∗} abort or ⟨c, (s, h_{0})⟩ ↑.

Syntax of Assertions

⟨assert⟩ ::= ⟨boolexp⟩

| ¬ ⟨assert⟩ | ⟨assert⟩ ∧ ⟨assert⟩ | ⟨assert⟩ ∨ ⟨assert⟩ | ⟨assert⟩ ⇒ ⟨assert⟩ | ⟨assert⟩ ⇔ ⟨assert⟩ | ∀⟨var⟩. ⟨assert⟩ | ∃⟨var⟩. ⟨assert⟩ | ⟨exp⟩ ↦ ⟨exp⟩ | emptyheap | ⟨assert⟩ ∗ ⟨assert⟩ | ⟨assert⟩ −∗ ⟨assert⟩

The Semantics of Assertions

[[−]]_{assert} ^{∈} ⟨assert⟩ → Stores → Heaps → B.
[[b]]_{assert}s h iff [[b]]_{boolexp}s,
[[ ¬ p]]_{assert}s h iff ¬[[p]]_{assert}s h,
[[p_{0} ∧ p_{1}]]_{assert}s h iff [[p_{0}]]_{assert}s h ∧ [[p_{1}]]_{assert}s h

(and similarly for ∨, ⇒, ⇔).

[[∀v. p]]_{assert}s h iff ∀x ^{∈} Z. [[p]]_{assert}([ s | v: x], h),
[[∃v. p]]_{assert}s h iff ∃x ^{∈} Z. [[p]]_{assert}([ s | v: x], h),

The Semantics of Assertions (continued)

[[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}

Examples

[[x + y = x]]_{assert}s h iff [[x + y = x]]_{boolexp}s
iff s y = 0.
[[∀x. x + y = x]]_{assert}s h iff ∀n ^{∈} Z. [[x + y = x]]_{assert}[ s | x: n] h
iff ∀n ^{∈} Z. [ s | x: n] y = 0
iff ∀n ^{∈} Z. s y = 0
iff s y = 0.
[[x ↦ y]]_{assert}s h iff dom h = {s x} and h(s x) = s y
iff h = {⟨s x, s y⟩}.

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
e ≐ e′ =^{def} (e = e′) ∧ emptyheap

Examples

[[x ↦ −]]_{assert}s h iff dom h = {s x}
[[x ↪ y]]_{assert}s h iff s x ^{∈} dom h and h(s x) = s y
[[x ↪ −]]_{assert}s h iff s x ^{∈} dom h
[[x ↦ y, z]]_{assert}s h iff h = {⟨s x, s y⟩, ⟨s x + 1, s z⟩}
[[x ↪ y, z]]_{assert}s h iff h ⊇ {⟨s x, s y⟩, ⟨s x + 1, s z⟩}
[[e ≐ e′]]_{assert}s h iff [[e]]_{exp}s = [[e′]]_{exp}s and dom h = {}

An Example of ∗

[[x ↦ 3, y ∗ y ↦ 4, x]]_{assert}s h

iff ∃h_{0}, h_{1}. h_{0} ⊥ h_{1} and h_{0} · h_{1} = h and [[x ↦ 3, y]]_{assert}s h_{0} and [[y ↦ 4, x]]_{assert}s h_{1}

x ↦ 3, y  [figure: 3; x; y]

y ↦ 4, x  [figure: 4; x; y]

x ↦ 3, y ∗ y ↦ 4, x [figure: 3; 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

An Example of −∗

[[x ↦ 7, 5 −∗ P]]_{assert}s h

iff ∀h′. (h′ ⊥ h and [[x ↦ 7, 5]]_{assert}s h′)

implies [[P]]_{assert}s (h · h′)

If:

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

then:

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

and:

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

Some Terminology

• When [[p]]_{assert}s h = true we say – p is true in (s, h),

– p holds for (s, h),

– p describes (s, h),

– (s, h) satisfies p.

• When [[p]]_{assert}s h = true for all states (s, h) ^{∈} States, we

say

– p is valid.

• When [[p]]_{assert}s h = false for all states (s, h) ^{∈} States, we

say

– p is unsatisfiable.

• When [[q]]_{assert}s h = true holds for every state (s, h) ^{∈}

States such that [[p]]_{assert}s h = true, we say – p is stronger than q,

– q is weaker than p. (Notice that true is weaker than any assertion and false is stronger than any assertion.)

• When [[q]]_{assert}s h = true holds for exactly those states

(s, h) ^{∈} States such that [[p]]_{assert}s h = true, we say – p is equivalent to q.

Substitution

Proposition 6 Let δ abbreviate the substitution

v_{1} → e_{1}, …, v_{n} → e_{n},

and for any store s, let

ŝ = [ v_{1}: [[e_{1}]]_{exp}s | … | v_{n}: [[e_{n}]]_{exp}s].

If p is an assertion whose free variables belong to {v_{1}, …, v_{n}}, then

[[p/δ]]_{assert}s h = [[p]]_{assert}ŝh.

Eventually, δ will map

ordinary variables into expressions
sequence variables into sequence expressions
tree variables into tree expressions
assertion variables into assertions
⋮

Inference Rules

• An inference rule consists of zero or more premisses and a single conclusion, separated by a horizontal line:

\frac{P_{1}  ⋯  P_{n}}{C}

• The premisses and conclusion are schemata, i.e., they may contain metavariables, each of which ranges over some set of phrases.

• An instance of an inference rule is obtained by replacing each metavariable by a phrase in its range (satisfying any side-conditions). In an instance, the premisses and conclusion will be assertions (or transitions or specifications).

• A formal proof is a sequence of assertions, each of which is the conclusion of some instance of an inference rule whose premisses occur earlier in the sequence.

• An inference rule with zero premisses is called an axiom schema. The overbar is sometimes omitted.

• An axiom schema containing no metavariables is called an axiom. The overbar is usually omitted.

Some Inference Rules

x + 0 = x (an axiom)

\overline{e_{1} = e_{0} ⇒ e_{0} = e_{1}}  (an axiom schema)

\frac{p p ⇒ q}{q}

\frac{p}{∀v. p}

Some Instances

x + 0 = x \overline{x + 0 = x ⇒ x = x + 0}

\frac{x + 0 = x x + 0 = x ⇒ x = x + 0}{x = x + 0}

\frac{x = x + 0}{∀x. x = x + 0}

A Formal Proof

1.  x + 0 = x  (First rule)
2.  x + 0 = x ⇒ x = x + 0  (Second rule)
3.  x = x + 0  (Third rule, 1, 2)
4.  ∀x. x = x + 0  (Fourth rule, 3)

\frac{\overline{x + 0 = x} \overline{x + 0 = x ⇒ x = x + 0}}{\frac{x = x + 0}{∀x. x = x + 0}}

Soundness

An inference rule is sound iff, for all instances,

• if the premisses of the instance are all valid (i.e. true in all states),

• then the conclusion is valid (i.e. true in all states). (It follows that the assertions in a formal proof must all be valid.) For example,

\frac{p}{∀v. p}

is sound, since for any assertion p and variable v, if p is true in all states, then ∀v. p is true in all states. However,

\overline{p ⇒ ∀v. p}

is not sound, since its instance

\overline{x > 0 ⇒ ∀x. x > 0}

has a conclusion that does not hold in a state that maps x into

Some Inference Rules for ⇒ and ¬

\frac{p p ⇒ q}{q}  (Modus Ponens)

\begin{aligned}p & ⇒ & (q ⇒ p) \\ (p ⇒ (q ⇒ r)) & ⇒ & ((p ⇒ q) ⇒ (p ⇒ r)) \\ (¬ q ⇒ ¬ p) & ⇒ & ((¬ q ⇒ p) ⇒ q) \end{aligned}

Other Connectives

\begin{aligned}(p ⇔ q) & ⇒ & (p ⇒ q) \\ (p ⇔ q) & ⇒ & (q ⇒ p) \\ (p ∧ q) & ⇔ & ¬(p ⇒ ¬ q) \\ (p ∨ q) & ⇔ & (¬ p) ⇒ q \\ (p ⇔ q) & ⇔ & (p ⇒ q) ∧ (q ⇒ p) \end{aligned}

Quantifiers

\frac{p}{∀v. p}  (Generalization)
(∀v. p) ⇒ (p/v → e)
(∀v. p ⇒ q) ⇔ (p ⇒ ∀v. q) when v is not free in p
(∃v. p) ⇔ ¬ (∀v. ¬ p)
(p/v → e) ⇒ (∃v. p)
(∃v. p ⇒ q) ⇔ (p ⇒ ∃v. q) when v is not free in p

Equality

\begin{aligned}e & = & e \\ e = e′ & ⇒ & e′ = e \\ e = e′ ∧ e′ = e′′ & ⇒ & e = e′′ \\ e_{1} = e_{2} & ⇒ & (e/v → e_{1}) = (e/v → e_{2}) \end{aligned}

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 ∗ x′ ↦ e′ ∗ true ⇒ x ≠ x′
emptyheap ⇔ ∀x. ¬(x ↦ − ∗ true)
(e ↪ x) ∧ p ⇒ (e ↦ x) ∗ ((e ↦ x) −∗ p).

Pure Assertions

An assertion is pure if it does not contain ↦ or emptyheap.

A pure assertion does not depend upon the heap.

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

Some Derived Inference Rules

\overline{q ∗ (q −∗ p) ⇒ p}

Derivation:

\frac{q ∗ (q −∗ p) ⇒ (q −∗ p) ∗ q \frac{(q −∗ p) ⇒ (q −∗ p)}{(q −∗ p) ∗ q ⇒ p}}{q ∗ (q −∗ p) ⇒ p}

\overline{r ⇒ (q −∗ (q ∗ r))}

Deriviation:

\frac{(r ∗ q) ⇒ (q ∗ r)}{r ⇒ (q −∗ (q ∗ r))}

\overline{(p ∗ r) ⇒ (p ∗ (q −∗ (q ∗ r)))}

Derivation:

\frac{p ⇒ p r ⇒ (q −∗ (q ∗ r))}{(p ∗ r) ⇒ (p ∗ (q −∗ (q ∗ r)))}

More Derived Inference Rules

\frac{p_{1} ⇒ (q −∗ r) p_{2} ⇒ (r −∗ s)}{p_{2} ∗ p_{1} ⇒ (q −∗ s)}

Derivation:

\frac{\frac{\overline{p_{2} ⇒ p_{2}}  \frac{p_{1} ⇒ (q −∗ r)}{p_{1} ∗ q ⇒ r}}{p_{2} ∗ p_{1} ∗ q ⇒ p_{2} ∗ r}  \frac{p_{2} ⇒ (r −∗ s)}{p_{2} ∗ r ⇒ s}}{\frac{p_{2} ∗ p_{1} ∗ q ⇒ s}{p_{2} ∗ p_{1} ⇒ (q −∗ s)}}
p′ ⇒ p q ⇒ q′
(p −∗ q) ⇒ (p′ −∗ q′).

Derivation:

\frac{\frac{\frac{\overline{(p −∗ q) ⇒ (p −∗ q)} p′ ⇒ p}{(p −∗ q) ∗ p′ ⇒ (p −∗ q) ∗ p} \frac{\overline{(p −∗ q) ⇒ (p −∗ q)}}{(p −∗ q) ∗ p ⇒ q}}{(p −∗ q) ∗ p′ ⇒ q} q ⇒ q′}{\frac{(p −∗ q) ∗ p′ ⇒ q′}{(p −∗ q) ⇒ (p′ −∗ q′)}}

Specifications

⟨spec⟩ ::= {⟨assert⟩} ⟨comm⟩ {⟨assert⟩} (partial correctness) | [ ⟨assert⟩] ⟨comm⟩ [ ⟨assert⟩] (total correctness)

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

Partial correctness: [[{p} c {q}]]_{spec} iff ∀(s, h) ^{∈} States. [[p]]_{assert}s h implies

¬ (c, (s, h) ⇝^{∗} abort) and (∀(s′, h′) ^{∈} States. c, (s, h) ⇝^{∗} (s′, h′) implies [[q]]_{assert}s′ h′)

Total correctness: [[[ p] c [ q ]]]_{spec} iff ∀(s, h) ^{∈} States. [[p]]_{assert}s h implies

¬ (c, (s, h) ⇝^{∗} abort) and ¬ (c, (s, h) ↑) and (∀(s′, h′) ^{∈} States. c, (s, h) ⇝^{∗} (s′, h′) implies [[q]]_{assert}s′ h′).

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

• An execution giving a memory fault falsifies a specification.

Examples of Partial Correctness Specifications

{x − y > 3} x := x − y {x > 3}
{x + y ≥ 17} x := x + 10 {x + y ≥ 27}
{x ≤ 10} while x ≠ 10 do x := x + 1 {x = 10}
{true} while x ≠ 10 do x := x + 1 {x = 10}
{x > 10} while x ≠ 10 do x := x + 1 {false}

{emptyheap} x := cons(1, 2) {x ↦ 1, 2} {x ↦ 1, 2} y := [x] ; [x + 1] := 3 {x ↦ 1, 3 ∧ y = 1}

Examples of Total Correctness Specifications

[ x − y > 3 ] x := x − y [ x > 3 ]
[ x + y ≥ 17 ] x := x + 10 [ x + y ≥ 27 ]
[ x ≤ 10 ] while x ≠ 10 do x := x + 1 [ x = 10 ]

[ emptyheap ] x := cons(1, 2) [ x ↦ 1, 2 ] [ x ↦ 1, 2 ] y := [x] ; [x + 1] := 3 [ x ↦ 1, 3 ∧ y = 1 ]

Violating Record Boundaries

Suppose P holds for a state (s, h), and C′ does not assign to x. Then

[ P ] C ; x := cons(1, 2) ; C′ ; [x + 2] := 3 ; C′′ [ Q]

cannot hold. For suppose the contrary. Then

⟨C, (s, h)⟩ ⇝^{∗} (s′, h′).

Let ℓ be such that ℓ, ℓ + 1, ℓ + 2 ∉ dom h′. Then

⟨x := cons(1, 2), (s′, h′)⟩ ⇝ ([ s′ | x: ℓ], [ h′ | ℓ: 1 | ℓ + 1: 2 ]), and

⟨C′, ([ s′ | x: ℓ], [ h′ | ℓ: 1 | ℓ + 1: 2 ])⟩ ⇝^{∗} (s′′, h′′),

where s′′x = ℓ and ℓ + 2 ∉ dom h′′. Then

⟨[x + 2] := 3, (s′′, h′′)⟩ ⇝ abort,

and

⟨[x + 2] := 3 ; C′′, (s′′, h′′)⟩ ⇝ abort,

contradicting the assumption.

Inference Rules for Specifications: Assignment (AS)

\overline{\{p/v → e\} v := e \{p\}}  \overline{[ p/v → e] v := e [ p]}

Instances

\overline{\{x − y > 3\} x := x − y \{x > 3\}} \overline{\{(2 × y) − y > 3\} x := 2 × y \{x − y > 3\}}

Inference Rules for Specifications:

Sequential Composition (SQ)

\frac{\{p\} c_{1} \{q\} \{q\} c_{2} \{r\}}{\{p\} c_{1} ; c_{2} \{r\}}  \frac{[ p] c_{1} [ q ] [ q ] c_{2} [ r]}{[ p] c_{1} ; c_{2} [ r]}

An Instance

\frac{\{(2 × y) − y > 3\} x := 2 × y \{x − y > 3\} \{x − y > 3\} x := x − y \{x > 3\}}{\{(2 × y) − y > 3\} x := 2 × y ; x := x − y \{x > 3\}}

Note

Except for while commands and recursive procedures, reasoning for partial and total correctness will be the same, and we will henceforth only give rules for partial correctness.

Inference Rules for Specifications: Strengthening Precedent (SP)

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

An Instance

\frac{y > 3 ⇒ (2 × y) − y > 3 \{(2 × y) − y > 3\} x := 2 × y ; x := x − y \{x > 3\}}{\{y > 3\} x := 2 × y ; x := x − y \{x > 3\}}

Weakening Consequent (WC)

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

An Instance

\frac{\{y > 3\} x := 2 × y ; x := x − y \{x > 3\} x > 3 ⇒ x ≥ 4}{\{y > 3\} x := 2 × y ; x := x − y \{x ≥ 4\}}

A Simple Proof

1. {(2 × y) − y > 3} x := 2 × y {x − y > 3} (AS)

2. {x − y > 3} x := x − y {x > 3} (AS)

3. {(2 × y) − y > 3} x := 2 × y ; x := x − y {x > 3} (SQ,1,2)

4. y > 3 ⇒ (2 × y) − y > 3 (VC)

5. {y > 3} x := 2 × y ; x := x − y {x > 3} (SP,4,3)

6. x > 3 ⇒ x ≥ 4 (VC)

7. {y > 3} x := 2 × y ; x := x − y {x ≥ 4} (WC,5,6)

A More Realistic Proof

1. {f = fib(k + 1) ∧ g = fib((k + 1) − 1) ∧ k + 1 ≤ n} k := k + 1 {f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n} (AS)

2. {f + t = fib(k + 1) ∧ g = fib((k + 1) − 1) ∧ k + 1 ≤ n} f := f + t {f = fib(k + 1) ∧ g = fib((k + 1) − 1) ∧ k + 1 ≤ n} (AS)

3. {f + t = fib(k + 1) ∧ g = fib((k + 1) − 1) ∧ k + 1 ≤ n} f := f + t ; k := k + 1 {f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n} (SQ,1,2)

4. {f + t = fib(k + 1) ∧ f = fib((k + 1) − 1) ∧ k + 1 ≤ n} g := f {f + t = fib(k + 1) ∧ g = fib((k + 1) − 1) ∧ k + 1 ≤ n} (AS)

5. {f + t = fib(k + 1) ∧ f = fib((k + 1) − 1) ∧ k + 1 ≤ n} g := f ; f := f + t ; k := k + 1 {f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n} (SQ,3,4)

A More Realistic Proof (continued)

6. {f + g = fib(k + 1) ∧ f = fib((k + 1) − 1) ∧ k + 1 ≤ n} t := g {f + t = fib(k + 1) ∧ f = fib((k + 1) − 1) ∧ k + 1 ≤ n} (AS)

7. {f + g = fib(k + 1) ∧ f = fib((k + 1) − 1) ∧ k + 1 ≤ n} t := g ; g := f ; f := f + t ; k := k + 1 {f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n} (SQ,5,6)

8. (f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n ∧ k ≠ n) ⇒

(f + g = fib(k + 1) ∧ f = fib((k + 1) − 1) ∧ k + 1 ≤ n)

(VC^{∗})

9. {f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n ∧ k ≠ n} t := g ; g := f ; f := f + t ; k := k + 1 {f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n} (SP,7,8)

∗since

fib(0) = 0  fib(1) = 1  fib(i) = fib(i − 1) + fib(i − 2).

Inference Rules for Specifications: Partial Correctness of while (WHP)

\frac{\{i ∧ b\} c \{i\}}{\{i\} while b do c \{i ∧ ¬ b\}}

Here i is the invariant.

An Instance

\frac{\{f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n ∧ k ≠ n\} t := g ; g := f ; f := f + t ; k := k + 1 \{f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n\}}{\{f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n\} while k ≠ n do (t := g ; g := f ; f := f + t ; k := k + 1) \{f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n ∧ ¬ k ≠ n\}}

Inference Rules for Specifications: Total Correctness of while (WHT)

\frac{[ i ∧ b ∧ e = v_{0} ] c [ i ∧ e < v_{0} ] (i ∧ b) ⇒ e ≥ 0}{[ i] while b do c [ i ∧ ¬ b]}

when v_{0} does not occur free in i, b, c, or e. Here i is the invariant, e is the variant, and v_{0} is a ghost variable.

An Instance

\frac{[f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n ∧ k ≠ n ∧ n − k = v_{0}] t := g ; g := f ; f := f + t ; k := k + 1 [f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n ∧ n − k < v_{0}] (f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n ∧ k ≠ n) ⇒ n − k ≥ 0}{[f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n] while k ≠ n do (t := g ; g := f ; f := f + t ; k := k + 1) [f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n ∧ ¬ k ≠ n]}

Inference Rules for Specifications: skip (SK)

\overline{\{p\} skip \{p\}}

Conditional (CD)

\frac{\{p ∧ b\} c_{0} \{q\} \{p ∧ ¬ b\} c_{1} \{q\}}{\{p\} if b then c_{0} else c_{1} \{q\}}

Inference Rules for Specifications:

Variable Declaration (DC)

\frac{\{p\} c \{q\}}{\{p\} newvar v in c \{q\}}

when v does not occur free in p or q.

Here the requirement on the declared variable v formalizes the concept of locality, i.e., that the value of v when c begins execution has no effect on this execution, and that the value of v when c finishes execution has no effect on the rest of the program.

Locality is a property of the specification of a command rather than just the command itself, since it depends on the use to which the command may be put. For example, the same command satisfies both of the specifications

{true} t := x + y ; z := t × t {z = (x + y)^{2}}
{true} t := x + y ; z := t × t {z = (x + y)^{2} ∧ t = x + y}.

But the variable t is local only in the first case, so that newvar t in (t := x + y ; z := t × t) meets only the first specification:

{true} newvar t in (t := x + y ; z := t × t) {z = (x + y)^{2}}.

Rules for Annotated Specifications: Sequential Composition (SQ)

\frac{\{p\} c_{1} \{q\} \{q\} c_{2} \{r\}}{\{p\} c_{1} ; \{q\} c_{2} \{r\}}

Strengthening Precedent (SP)

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

Weakening Consequent (WC)

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

Rules for Annotated Specifications: Assignment (AS)

\frac{p_{0} ⇒ (p/v → e)}{\{p_{0}\} v := e \{p\}}  \frac{\{p_{0}\} c \{p/v → e\}}{\{p_{0}\} c; v := e \{p\}}

skip (SK)

\frac{p_{0} ⇒ p}{\{p_{0}\} skip \{p\}}

Partial Correctness of while (WHP)

\frac{\{i ∧ b\} c \{i\} (i ∧ ¬ b) ⇒ p}{\{i\} while b do c \{p\}}

Total Correctness of while (WHT)

\frac{[ i ∧ b ∧ e = v_{0} ] c [ i ∧ e < v_{0} ] (i ∧ b) ⇒ e ≥ 0 (i ∧ ¬ b) ⇒ p}{[ i] while [vrnt: e] b do c [ p]}

when v_{0} does not occur free in i, b, c, or e. The rules for conditionals and variable declarations remain unchanged.

An Annotated Specification

[n ≥ 0] if n = 0 then f := 0 else

newvar g in newvar k in (k := 1 ; g := 0 ; f := 1 ; [f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n] while [vrnt: n − k] k ≠ n do

(t := g ; g := f ; f := f + t ; k := k + 1)) [f = fib(n)]

Structural Inference Rules:

Renaming (RN)

\frac{\{p\} c \{q\}}{\{p′\} c′ \{q′\},}

where p′, c′, and q′ are obtained from p, c, and q by zero or more renamings of subphrases.

Free Variable Substitution (FVS)

{p} c {q}
({p} c {q})/v_{1} → e_{1}, …, v_{n} → e_{n},

where v_{1}, …, v_{n} are the variables occurring free in p, c, or q, and, if v_{i} is assigned by c, then e_{i} is a variable that does not occur free in any other e_{j}.

For example, in

{x = y} x := x + y {x = 2 × y},

one can substitute x, y → z, 2 × w − 1 to infer

{z = 2 × w − 1} z := z + 2 × w − 1 {z = 2 × (2 × w − 1)}.

But one cannot substitute x, y → z, 2 × z − 1 to infer

{z = 2 × z − 1} z := z + 2 × z − 1 {z = 2 × (2 × z − 1)}.

Free Variable Substitution (continued)

{p} c {q}
({p} c {q})/v_{1} → e_{1}, …, v_{n} → e_{n},

where v_{1}, …, v_{n} are the variables occurring free in p, c, or q, and, if v_{i} is assigned by c, then e_{i} is a variable that does not occur free in any other e_{j}.

Proposition 7 The free variable substitution rule is sound.

Proof Let δ abbreviate the substitution

v_{1} → e_{1}, …, v_{n} → e_{n},

and for any store s, let

ŝ = [ v_{1}: [[e_{1}]]_{exp}s | … | v_{n}: [[e_{n}]]_{exp}s].

• Assume {p} c {q} and [[p/δ]]_{assert}s h. By Proposition 6, [[p]]_{assert}ŝh.

• Suppose ⟨c/δ, (s, h)⟩ ⇝^{∗} abort. By Proposition 4, we would have ⟨c, (ŝ, h)⟩ ⇝^{∗} abort, which contradicts {p} c {q} and [[p]]_{assert}ŝh.

• Suppose ⟨c/δ, (s, h)⟩ ⇝^{∗} (s′, h′). By Proposition 4, we have ⟨c, (ŝ, h)⟩ ⇝^{∗} (ŝ′, h′), so that {p} c {q} and [[p]]_{assert}ŝh give [[q]]_{assert}ŝ′h′. Then, by Proposition 6, [[q/δ]]_{assert}s′h′.

end of proof

Structural Inference Rules: Disjunction of Assertions (DA)

\frac{\{p_{0}\} c \{q_{0}\} \{p_{1}\} c \{q_{1}\}}{\{p_{0} ∨ p_{1}\} c \{q_{0} ∨ q_{1}\}}

Conjunction of Assertions (CA)

\frac{\{p_{0}\} c \{q_{0}\} \{p_{1}\} c \{q_{1}\}}{\{p_{0} ∧ p_{1}\} c \{q_{0} ∧ q_{1}\}}

Existential Quantification of Assertions (EQ)

\frac{\{p\} c \{q\}}{\{∃v. p\} c \{∃v. q\}} ,

Universal Quantification of Assertions (UQ)

\frac{\{p\} c \{q\}}{\{∀v. p\} c \{∀v. q\}} ,

where v is not free in c.

where v is not free in c.

Structural Inference Rules: The Unsound Rule of Constancy

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

when no variable occurs both free in r and assigned by c.

Counterexamples

\frac{\{x = y ∧ x ↦ 3\} [x] := 4 \{x = y ∧ x ↦ 4\}}{\{x = y ∧ x ↦ 3 ∧ y ↦ 3\} [x] := 4 \{x = y ∧ x ↦ 4 ∧ y ↦ 3\}}

\frac{\{x ↦ 3\} [x] := 4 \{x ↦ 4\}}{\{x ↦ 3 ∧ x ↦ 3\} [x] := 4 \{x ↦ 4 ∧ x ↦ 3\}}

Structural Inference Rules:

The Frame Rule (FR)

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

when no variable occurs both free in r and assigned by c.

Proposition 8 The frame rule is sound.

Proof

• Assume {p} c {q}, and [[p ∗ r]]_{assert}s h. Then there are h_{0}, h_{1} such that h_{0} ⊥ h_{1}, h = h_{0} · h_{1}, [[p]]_{assert}s h_{0} and [[r]]_{assert}s h_{1}.

• Suppose ⟨c, (s, h)⟩ ⇝^{∗} abort. Then, by Proposition 5, we would have ⟨c, (s, h_{0})⟩ ⇝^{∗} abort, which contradicts {p} c {q} and [[p]]_{assert}s h_{0}.

• Suppose ⟨c, (s, h)⟩ ⇝^{∗} (s′, h′). Again, ⟨c, (s, h_{0})⟩ ⇝^{∗} abort would contradict {p} c {q} and [[p]]_{assert}s h_{0}, so that, by Proposition 5, ⟨c, (s, h_{0})⟩ ⇝^{∗} (s′, h′_{0}), where h′_{0} ⊥ h_{1} and h′ = h′_{0} · h_{1}. Then {p} c {q} and [[p]]_{assert}s h_{0} imply that [[q]]_{assert}s′h′_{0}.

• Since ⟨c, (s, h)⟩ ⇝^{∗} (s′, h′), Proposition 3 gives s v = s′v for all v that are not assigned by c. Then, since these include the free variables of r, [[r]]_{assert}s h_{1} implies that [[r]]_{assert}s′h_{1}. Thus [[q ∗ r]]_{assert}s′h.

end of proof

Inference Rules for Mutation

The small form:

\overline{\{e ↦ −\} [e] := e′ \{e ↦ e′\}.}  (1)

The large form:

\overline{\{(e ↦ −) ∗ r\} [e] := e′ \{(e ↦ e′) ∗ r\}.}  (2)

The WP form:

\overline{\{(e ↦ −) ∗ ((e ↦ e′) −∗ p)\} [e] := e′ \{p\}.}  (3)

One can derive (2) from (1) by using the frame rule; one can go in the opposite direction by taking r to be emptyheap. One can derive (3) from (2) by taking r to be (e ↦ e′) −∗ p and using the law q ∗ (q −∗ p) ⇒ p:

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

[e] := e′

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

{p}. One can go in the opposite direction by taking p to be (e ↦ e′) ∗ r and using the law (p ∗ r) ⇒ (p ∗ (q −∗ (q ∗ r))):

{(e ↦ −) ∗ r}

{(e↦−) ∗ ((e↦e′) −∗ ((e↦e′) ∗ r))}

[e] := e′

{(e↦e′) ∗ r}.

Inference Rules for Noninterfering Allocation

The small form:

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

(4)

where v ∉ FV(e_{0}, …, e_{n−1}).

The large form:

\overline{\{r\} v := cons(e_{0}, …, e_{n−1}) \{(v ↦ e_{0}, …, e_{n−1}) ∗ r\},} (5)

where v ∉ FV(e_{0}, …, e_{n−1}, r).

One can derive (5) from (4) by using the frame rule; one can go in the opposite direction by taking r to be emptyheap.

Inference Rules for General Allocation

We assume that v, v′, and v′′ are distinct variables, and, for any phrase p, we write p′ for p/v → v′ and p′′ for p/v → v′′. The small form:

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

(6)

The large form:

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

where v′ ∉ FV(e_{0}, …, e_{n−1}, r). The WP form: \overline{\{∀v′′. (v′′ ↦ e_{0}, …, e_{n−1}) −∗ p′′\} v := cons(e_{0}, …, e_{n−1}) \{p\},}

(8)

where v′′ ∉ FV(e_{0}, …, e_{n−1}, p). Let \overline{e} abbreviate e_{0}, …, e_{n−1}, and \overline{e}′ abbreviate e′_{0}, …, e′_{n−1}. One can derive (7) from (6) by using the frame rule and (EQ):

{v = v′ ∧ r′}

{(v = v′ ∧ emptyheap) ∗ r′} v := cons(\overline{e}) \{(v ↦ \overline{e}′) ∗ r′\},

\{r\} \{∃v′. v = v′ ∧ r′\} v := cons(\overline{e}) \{∃v′. (v ↦ \overline{e}′) ∗ r′\}.

Inference Rules for General Allocation (continued)

To derive (8) from (7), we choose v′ ∉ FV(e_{0}, …, e_{n−1}, p), take r to be ∀v′′. (v′′ ↦ \overline{e}) −∗ p′′, and use various laws about quantifiers, as well as q ∗ (q −∗ p) ⇒ p:

\{∀v′′. (v′′ ↦ \overline{e}) −∗ p′′\}
v := cons(\overline{e})
\{∃v′. (v ↦ \overline{e}′) ∗ (∀v′′. (v′′ ↦ \overline{e}′) −∗ p′′)\}
\{∃v′. (v ↦ \overline{e}′) ∗ ((v ↦ \overline{e}′) −∗ p)\}
{∃v′. p}
{p}.

To go in the other direction, we choose v′′ ∉ FV(e_{0}, …, e_{n−1}, r), take p to be ∃v′. (v ↦ \overline{e}′) ∗ r′, and use various laws about quantifiers, as well as r ⇒ (q −∗ (q ∗ r)):

{r}
{∀v′′. r}
\{∀v′′. (v′′ ↦ \overline{e}) −∗ ((v′′ ↦ \overline{e}) ∗ r)\}
\{∀v′′. (v′′ ↦ \overline{e}) −∗ (∃v′. (v′′ ↦ \overline{e}′) ∗ r′)\}
v := cons(\overline{e})
\{∃v′. (v ↦ \overline{e}′) ∗ r′\}.

Inference Rules for Disposal

The small form:

{e ↦ −} dispose e {emptyheap}.

(9)

The large (WP) form:

\overline{\{(e ↦ −) ∗ r\} dispose e \{r\}.}  (10)

One can derive (10) from (9) by using the frame rule; one can go in the opposite direction by taking r to be emptyheap.

Inference Rules for Lookup

The small form:

\overline{\{(e ↦ v′′) ∧ v = v′\} v := [e] \{v = v′′ ∧ (e′ ↦ v′′)\},}  (11)

where v, v′, and v′′ are distinct variables. The large (WP) form:

\overline{\{∃v′′. (e ↪ v′′) ∧ p′′\} v := [e] \{p\},}  (12)

where v′′ does not occur free in p or e, and p′′ is p/v → v′′. To derive (12) from (11), we use the frame rule and the rule for existential quantification (EQ), and then use the implications (e ↪ x) ∧ p ⇒ (e ↦ x) ∗ ((e ↦ x) −∗ p) and q ∗ (q −∗ p) ⇒ p:

{∃v′′. (e ↪ v′′) ∧ p′′} {∃v′′. (e ↦ v′′) ∗ ((e ↦ v′′) −∗ p′′)} {∃v′, v′′. ((e ↦ v′′) ∧ v = v′) ∗ ((e′ ↦ v′′) −∗ p′′)} v := [e] {∃v′, v′′. (v = v′′ ∧ (e′ ↦ v′′)) ∗ ((e′ ↦ v′′) −∗ p′′)} {∃v′, v′′. v = v′′ ∧ p′′} {∃v′, v′′. p} {p}.

Inference Rules for Lookup (continued)

To derive (11) from (12), we rename v′′ in (12) to a fresh variable v′′′ that is distinct from v, v′, or v′′ and does not occur free in e. Then we take p to be v = v′′ ∧ e′ ↦ v′′:

{(e ↦ v′′) ∧ v = v′} {(e ↦ v′′) ∧ (e′ ↦ v′′)} {(e ↪ v′′) ∧ (e′ ↦ v′′)} {∃v′′′. (e ↪ v′′′) ∧ (v′′′ = v′′ ∧ e′ ↦ v′′)} v := [e] {v = v′′ ∧ e′ ↦ v′′}.

An Annotated Specification

{emptylist} x := cons(a, a) ; {x ↦ a, a} y := cons(b, b) ; {x ↦ a, a ∗ y ↦ b, b} [x + 1] := y − x ; {x ↦ a, y − x ∗ y ↦ b, b} [y + 1] := x − y ; {x ↦ a, y − x ∗ y ↦ b, x − y} {∃o. x ↦ a, o ∗ y ↦ b, −o}

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

Proof of the Composition Property

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

The proof is by induction on the length of α. When α is empty:

∃j. list ϵ (i, j) ∗ list β (j, k) ⇔ ∃j. (emptyheap ∧ i = j) ∗ list β (j, k) ⇔ ∃j. (emptyheap ∗ list β (j, k)) ∧ i = j ⇔ ∃j. list β (j, k) ∧ i = j ⇔ list β (i, k) ⇔ list ϵ·β (i, k)

When α = a·α′:

∃j. list a·α′ (i, j) ∗ list β (j, k) ⇔ ∃j, l. i ↦ a, l ∗ list α′ (l, j) ∗ list β (j, k) ⇔ ∃l. i ↦ a, l ∗ list α′·β (l, k) (induction hypothesis) ⇔ list a·α′·β (i, 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 ↦ a, j ∗ list α (j, k))} {∃j. (i ↦ a, j ∗ list α (j, k)) ∧ (i ↦ a, j ∗ true)} {∃j. (i ↦ a, j ∗ list α (j, k)) ∧ (i ↦ a ∗ i + 1 ↦ j ∗ true)} {∃j. (i ↦ a, j ∗ list α (j, k)) ∧ (true ∗ i + 1 ↦ j ∗ true)} {∃j. (i ↦ a, j ∗ list α (j, k)) ∧ (i + 1 ↦ j ∗ true)} {∃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)}

Deleting a List Element (continued)

• 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} )

Xor-Linked Lists

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

Xor-Linked Lists

xlist α (i, i′, j, j′):  [figure: i′; α_{1}; i; ⋯; ⋯; j; α_{n}; j′]
xlist ϵ (i, i′, j, j′) =^{def} emptyheap ∧ i = j ∧ i′ = j′
xlist a·α (i, i′, k, k′) =^{def} ∃j. i ↦ a, (j ⊕ i′) ∗ xlist α (j, i, k, k′).

Properties

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

Emptyness Conditions

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