Lectures on Reasoning about Shared Mutable Data Structure

John C. Reynolds Department of Computer Science

Carnegie Mellon University

Tandil, Argentina September 2000

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] (who 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; it is this extension that will be used in these lectures. We will begin with the denotational semantics of predicate logic and a transition-based operational semantics of the simple imperative language, whose marriage will give traditional Hoare logic. (A more detailed presentation can be found in [17].) Then we will extend the programming language with new commands for dealing with shared mutable structure, extend predicate calculus with new assertions and operations for describing such structure, and add inference rules to Hoare logic to support reasoning about these extensions. Finally, we will use inductive definitions for predicates on abstract data types to define singly and doubly-linked lists, which be used in a variety of examples. The research of my own that is described in these lectures was supported by National Science Foundation Grant CCR–9804014.

The diagrams on pages 68 and 72 are used with the kind permission of Peter O’Hearn.

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 Millennial Perspectives in Computer Science. Palgrave, 2000.

[21] Samin Ishtiaq and Peter W. O’Hearn. BI as an assertion language for mutable data structure. To appear in POPL 2001, March 10, 2000.

[22] David Walker and Greg Morrisett. Alias types for recursive data structures. In Workshop on Types in Compilation,

An Abstract Grammar for Predicate Logic

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

⟨assert⟩ ::= true | false | ⟨exp⟩ = ⟨exp⟩ | ⟨exp⟩ ≠ ⟨exp⟩ | ⋯ | ¬ ⟨assert⟩ | ⟨assert⟩ ∧ ⟨assert⟩ | ⟨assert⟩ ∨ ⟨assert⟩ | ⟨assert⟩ ⇒ ⟨assert⟩ | ⟨assert⟩ ⇔ ⟨assert⟩ | ∀⟨var⟩. ⟨assert⟩ | ∃⟨var⟩. ⟨assert⟩

Concrete Representation

• In decreasing order of precedence:

× (−_{unary} + −_{binary}) (= ≠ ↦ ↪) ¬ (∧ ∗) ∨ (⇒ −∗) ⇔ := ;

• Each of the binary operators is left associative.

• A quantified expression ∀v. a or ∃v. a may follow any boolean operator, and will extend to the first stopping symbol, i.e.

– an unmatched closing delimiter:

) ] } : | do else in then

– or, when unparenthesized by any delimiters:

; ,

or to the end of the enclosing phrase. For example,

(y + 1 = z ∧ ∀x. x = 0 ∨ x ≠ 0) ⇔ y = z − 1 is ([[y + 1] = z] ∧ [∀x. [[x = 0] ∨ [x ≠ 0]]]) ⇔ [y = [z − 1]].

The Denotational Semantics of Predicate Logic

Let States be the set of states

States = ⟨var⟩ → Z,

where

Z = {…, −2, −1, 0, 1, 2, …} B = {true, false}. Then the semantic functions

[[−]]_{exp} ^{∈} ⟨exp⟩ → States → Z
[[−]]_{assert} ^{∈} ⟨assert⟩ → States → B

are defined by semantic equations.

The Semantic Equations

[[0]]_{exp}σ = 0 (and similarly for 1, 2, ... ),
[[v]]_{exp}σ = σv,
[[ − e]]_{exp}σ = − [[e]]_{exp}σ,
[[e_{0} + e_{1}]]_{exp}σ = [[e_{0}]]_{exp}σ + [[e_{1}]]_{exp}σ

(and similarly for −, ×, …),

[[true]]_{assert}σ = true,
[[false]]_{assert}σ = false,
[[e_{0} = e_{1}]]_{assert}σ = ([[e_{0}]]_{exp}σ = [[e_{1}]]_{exp}σ)

(and similarly for ≠, …),

[[ ¬ p]]_{assert}σ = ¬[[p]]_{assert}σ,
[[p_{0} ∧ p_{1}]]_{assert}σ = [[p_{0}]]_{assert}σ ∧ [[p_{1}]]_{assert}σ

(and similarly for ∨, ⇒, ⇔),

[[∀v. p]]_{assert}σ = ∀n ^{∈} Z. [[p]]_{assert}[ σ | v: n],
[[∃v. p]]_{assert}σ = ∃n ^{∈} Z. [[p]]_{assert}[ σ | v: n].

An Example

Suppose σ x = 3. Then:

[[x + 0 = x]]_{assert}σ = ([[x + 0]]_{exp}σ = [[x]]_{exp}σ)
= ([[x]]_{exp}σ + [[0]]_{exp}σ = [[x]]_{exp}σ)
= (3 + 0 = 3)
= true.

Moreover, the above argument does not depend on the choice of 3; it holds for any integer n that x might be mapped into by σ. Thus, for any state σ,

[[∀x. x + 0 = x]]_{assert}σ = ∀n ^{∈} Z. [[x + 0 = x]]_{assert}[ σ | x: n]
= true.

Some Terminology

• When [[p]]_{assert}σ = true we say – p is true in σ,

– p holds for σ,

– p describes σ,

– σ satisfies p.

• When [[p]]_{assert}σ = true for all states σ ^{∈} States, we say – p is valid.

• When [[p]]_{assert}σ = false for all states σ ^{∈} States, we say – p is unsatisfiable.

• When [[q]]_{assert}σ = true holds for every state σ ^{∈} States

such that [[p]]_{assert}σ = 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}σ = true holds for exactly those states σ ^{∈}

States such that [[p]]_{assert}σ = true, we say – p is equivalent to q.

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 later, 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

Binding

• Certain occurrences of variables are binders, each of which has an associated phrase called its scope.

– In predicate logic, the first occurrence of v in ∀v. p or ∃v. p is a binder, and its scope is p.

– In a programming language with local variable declarations, the first occurrences of v in newvar v := e in c is a binder and its scope is c.

• If an occurrence of v (which is not itself a binder) lies within the scope of a binder of v, it is said to be bound by the binder; otherwise, it is a free occurrence.

• When the occurrence of v lies within the scopes of several binders of v, it is bound by the one with the smallest scope.

• We write FV_{exp}(p) or FV_{assert}(p) for the set of variables that occur free in p.

For example:

∀ {x \atop 1} . ( \begin{matrix}x \\ 1 \end{matrix} ≠ y ∨ ∀ {y \atop 2} . ( \begin{matrix}x \\ 1 \end{matrix} = {y \atop 2} ∨ ∀ {x \atop 3} . {x \atop 3} + {y \atop 2} ≠ \begin{matrix}x \\ 3 \end{matrix} ))

FV_{assert}(∀x. x + y ≠ x) = {y}
FV_{assert}(x = y ∨ ∀x. x + y ≠ x) = {x, y}

Renaming

• If v_{new} ∉ FV_{assert}(p) − {v}, then

∀v_{new}. (p/v → v_{new})

is said to be a renaming of

∀v. p.

• If v_{new} ∉ FV_{comm}(c) − {v}, then

newvar v_{new} := e in (c/v → v_{new})

is said to be a renaming of

newvar v := e in c.

For all languages considered in these lectures, renaming preserves meaning.

Substitution

Consider the sound inference rule

\overline{(∀v. p) ⇒ (p/v → e)} ,

where p/v → e denotes the result of substituting e for v in p. Suppose we replace

p by ∃y. y > x
v by x
e by y + 1

to obtain the instance

(∀x. ∃y. y > x) ⇒ ((∃y. y > x)/x → y + 1).

If the substitution x → y + 1 merely replaces x by y + 1, we get

(∀x. ∃y. y > x) ⇒ (∃y. y > y + 1),

which is clearly false. Instead, before we carry out the substitution, we must rename the binder y in the second occurrence of ∃y. y > x so that it does not capture the occurrence of y in y + 1:

(∀x. ∃y. y > x) ⇒ ((∃z. z > x)/x → y + 1).

Then the substitution gives the correct result

(∀x. ∃y. y > x) ⇒ (∃z. z > y + 1).

In general, before carrying out the substitution p/v → e one must rename subphrases of p so that no variable occurring free in e occurs as a binder in p (whose scope encloses a free occurrence of v).

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}

Exercise 1.1

State the following in predicate logic:

1. There is at least one integer larger than zero and smaller than two.

2. There is at most one integer larger than zero and smaller than two.

3. There are at least two distinct integers larger than zero and smaller than three.

4. There are at most two distinct integers larger than zero

and smaller than three. State the following in predicate logic. Assume that variables and expressions only range over natural numbers (that is, nonnegative integers). Do not use the operations ÷ or rem.

1. a is a divisor of b (or, equally well, b is a multiple of a).

2. a is a common divisor of b and c.

3. a is a greatest common divisor of b and c.

4. p is prime.

Exercise 1.2

Suppose that, when v is a variable and e_{0}, e_{1}, and e_{2} are integer expressions,

sum v: e_{0} to e_{1}. e_{2}

is an integer expression (called a summation expression) with the same meaning as the conventional mathematical expression

∑_{v=e_{0}}^{e_{1}} e_{2}.

Describe this extension of predicate logic by giving:

1. an abstract-grammar production;

2. a semantic equation;

3. a definition of any binders and their scopes;

4. some nontrivial inference rules.

The Simple Imperative Language: Abstract Syntax

⟨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⟩:= ⟨exp⟩ in ⟨comm⟩

Structural Operational Semantics

An execution (of a command) is a sequence

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

where each configuration γ_{i} is either of: • A state (a terminal configuration)

• A state paired with a command (a nonterminal configura-

tion) 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 ].

Configurations and the Transition Relation

In general, we have

• Γ_{N} = ⟨comm⟩ × States: the set of nonterminal configurations,

• Γ_{T} = States: the set of terminal configurations,

• Γ = Γ_{N} ∪ Γ_{T}: the set of all configurations,

• ⇝: the transition relation between Γ_{N} and Γ,

• executions, which are finite or infinite sequences of configurations, each of which is related to the next by the transition relation,

• the transitive and reflexive closure, γ ⇝^{∗} γ′, which holds if there is a finite execution beginning with γ and ending with γ′,

• γ ↑, which holds if γ diverges, i.e. if there is an infinite

execution beginning with γ. The transition relation will be defined by inference rules.

Totality

• 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.

• For every configuration γ, there is at least one execution sequence beginning with γ that is either infinite or ends with a terminal configuration.

Transition Rules for the Simple Imperative Language

• Assignment

\overline{⟨v := e, σ⟩ ⇝ [ σ | v: [[e]]_{exp}σ]}
• skip
\overline{⟨skip, σ⟩ ⇝ σ}

• Sequencing

\frac{⟨c_{0}, σ⟩ ⇝ σ′}{⟨c_{0} ; c_{1}, σ⟩ ⇝ ⟨c_{1}, σ′⟩}

\frac{⟨c_{0}, σ⟩ ⇝ ⟨c′_{0}, σ′⟩}{⟨c_{0} ; c_{1}, σ⟩ ⇝ ⟨c′_{0} ; c_{1}, σ′⟩}

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 and while Commands

• Conditional

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

⟨if b then c_{0} else c_{1}, σ⟩ ⇝ ⟨c_{0}, σ⟩

When [[b]]_{boolexp}σ = false:

⟨if b then c_{0} else c_{1}, σ⟩ ⇝ ⟨c_{1}, σ⟩

• while

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

⟨while b do c, σ⟩ ⇝ ⟨c; while b do c, σ⟩ When [[b]]_{boolexp}σ = false:

\overline{⟨while b do c, σ⟩ ⇝ σ}

Exercise 2.1

Let c be the command

while x ≠ 0 do if x = 1 then skip else x := x − 2.

1. Give an execution that begins with the configuration ⟨c, [ x: 2 ]⟩.

2. Prove the second transition of this execution.

Exercise 2.2

A repeat command has the form repeat c until b. Its effect is described by the following flowchart:

[figure: enter; c; b; exit; false; true]

Describe the syntax and semantics of this command by giving an abstract-grammar production and transition rules.

Specifications:

Syntax

⟨spec⟩ ::= {⟨precedent⟩} ⟨comm⟩ {⟨consequent⟩}

(partial correctness)

| [ ⟨precedent⟩] ⟨comm⟩ [ ⟨consequent⟩]

(total correctness)

⟨precedent⟩ ::= ⟨assert⟩
⟨consequent⟩ ::= ⟨assert⟩

Semantics

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

[[{p} c {q}]]_{spec} iff ∀σ ^{∈} States. [[p]]_{assert}σ implies (∀σ′. c, σ ⇝^{∗} σ′ implies [[q]]_{assert}σ′)

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

¬ c, σ ↑

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

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}

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 ]

Inference Rules: 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: 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\}}

Inference Rules: Strengthening Precedent (SP)

\frac{p ⇒ q \{q\} c \{r\}}{\{p\} c \{r\}}  \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\}}  \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: 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: 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: skip (SK)

\overline{\{p\} skip \{p\}}  \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\}}

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

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 ⇒ p′}{\{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\}}

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

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

Total Correctness of while (WHT)

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

when v_{0} does not occur free in p, b, c, or e.

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

Proof of an Annotated Specification

1. (n ≥ 0 ∧ n = 0) ⇒ 0 = fib(n) (VC)

2. [ n ≥ 0 ∧ n = 0 ] f := 0 [ f = fib(n) ] (AS1,1)

3. (n ≥ 0 ∧ ¬ n = 0)

⇒ (1 = fib(1) ∧ 0 = fib(1 − 1) ∧ 1 ≤ n) (VC)

4. [n ≥ 0 ∧ ¬ n = 0] k := 1 [1 = fib(k) ∧ 0 = fib(k − 1) ∧ k ≤ n] (AS1,3)

5. [n ≥ 0 ∧ ¬ n = 0] k := 1 ; g := 0 [1 = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n] (AS2,4)

6. [n ≥ 0 ∧ ¬ n = 0] k := 1 ; g := 0 ; f := 1 [f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n] (AS2,5)

Proof of an Annotated Specification (continued)

7. (f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n ∧ k ≠ n ∧ n − k = v_{0})

⇒ (f + g = fib(k + 1) ∧ f = fib((k + 1) − 1) ∧ k + 1 ≤ n ∧ n − (k + 1) < v_{0}) (VC)

8. [f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n ∧ k ≠ n ∧ n − k = v_{0}] t := g [f + t = fib(k + 1) ∧ f = fib((k + 1) − 1) ∧ k + 1 ≤ n

∧ n − (k + 1) < v_{0}] (AS1,7)

9. [f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n ∧ k ≠ n ∧ n − k = v_{0}] t := g ; g := f [f + t = fib(k + 1) ∧ g = fib((k + 1) − 1) ∧ k + 1 ≤ n

∧ n − (k + 1) < v_{0}] (AS2,8)

10. [f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n ∧ k ≠ n ∧ n − k = v_{0}] t := g ; g := f ; f := f + t [f = fib(k + 1) ∧ g = fib((k + 1) − 1) ∧ k + 1 ≤ n

∧ n − (k + 1) < v_{0}] (AS2,9)

11. [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}]

(AS2,10)

Proof of an Annotated Specification (continued)

12. (f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n ∧ k ≠ n) ⇒ n − k ≥ 0 (VC)

13. (f = fib(k) ∧ g = fib(k − 1) ∧ k ≤ n ∧ ¬ k ≠ n) ⇒ f = fib(n) (VC)

14. [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)] (WHT,11,12,13)

15. [n ≥ 0 ∧ ¬ n = 0] 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)] (SQ,6,14)

16. [n ≥ 0]

if n = 0 then f := 0 else (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)] (CD,2,15)

An Annotated Program for Fast Exponentiation

[n ≥ 0] k := n ; z := x ; y := 1; [y × z^{k} = x^{n} ∧ k ≥ 0] while [vrnt: k] k ≠ 0 do

if even k then (k := k ÷ 2 ; z := z × z)

else (k := k − 1 ; y := y × z) [y = x^{n}]

Verification Conditions

(n ≥ 0) ⇒ (1 × x^{n} = x^{n} ∧ n ≥ 0)

(y × z^{k} = x^{n} ∧ k ≥ 0 ∧ k ≠ 0 ∧ k = k_{0} ∧ even k) ⇒ (y × (z × z)k ÷ 2 = x^{n} ∧ k ÷ 2 ≥ 0 ∧ k ÷ 2 < k_{0})

(y × z^{k} = x^{n} ∧ k ≥ 0 ∧ k ≠ 0 ∧ k = k_{0} ∧ ¬ even k) ⇒ ((y × z) × zk − 1 = x^{n} ∧ k − 1 ≥ 0 ∧ k − 1 < k_{0})

(y × z^{k} = x^{n} ∧ k ≥ 0 ∧ k ≠ 0) ⇒ k ≥ 0

(y × z^{k} = x^{n} ∧ k ≥ 0 ∧ ¬ k ≠ 0) ⇒ y = x^{n}

Additional Inference Rules:

Variable Declaration (DC)

\frac{\{p\} c_{1} ; ⋯; c_{n} ; v := e; c \{q\}}{\{p\} c_{1} ; ⋯; c_{n} ; newvar v := e in c \{q\}}

\frac{[ p] c_{1} ; ⋯; c_{n} ; v := e; c [ q ]}{[ p] c_{1} ; ⋯; c_{n} ; newvar v := e in c [ q ]}

when v does not occur free in q and n ≥ 0.

Here the requirement on v formalizes the concept of locality, i.e., that the value of the declared variable plays no further role after execution of the scope of the declaration. 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 := x + y in z := t × t meets only the first specification:

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

Additional Inference Rules:

Renaming (RN)

\frac{\{p\} c \{q\}}{\{p′\} c′ \{q′\}}  \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.

Changing Free Variables (CF)

{p} c {q}
({p} c {q})/v_{1} → v′_{1}, …, v_{n} → v′_{n},

where v_{1}, …, v_{n} are the variables occurring free in p, c, or q, and v′_{1}, …, v′_{n} are distinct.

Additional Inference Rules:

Conjunction of Assertions (CA)

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

Disjunction of Assertions (DA)

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

Constancy for Partial Correctness (CSP)

\overline{\{p\} c \{p\}}

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

Constancy for Total Correctness (CST)

\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.

Exercise 3.1

Fill in the missing precedents indicated by question marks to make the following specifications true. The assertions that you provide should be as weak as possible, but they should not be unnecessarily complicated.

[ ? ] x := x + 1 ; y := y + 2 × x − 1 [ y = x^{2} ] [ ? ] x := x + y ; y := x − y ; x := x − y [ x = z ∧ y = w ] [ ? ] while a < b do (a := a + 1 ; y := x + y) [ y = x × b ] {?} while true do skip {false} [ ? ] while true do skip [ false ].

Exercise 3.2: Logarithmic-Time Multiplication

Complete the following “skeleton” by replacing the remarks in quotation marks. The result should be a correct annotated totalcorrectness specification (of a program that does not assign to the input variables x or y). You may use multiplication or division by two as a primitive operation but not multiplication or division by an arbitrary number.

[y ≥ 0]

“Achieve invariant” ;

[z + w × k = x × y ∧ k ≥ 0]

while [vrnt: k] k ≠ 0 do “Preserve invariant” [z = x × y]

Give the verification conditions needed to prove the annotated specification.

Exercise 3.3: Logarithmic-Time Division

Complete the following “skeleton” by replacing the remarks in quotation marks. The result should be a correct annotated totalcorrectness specification (of a program that does not assign to the input variables x or y). You may use multiplication or division by two as a primitive operation but not multiplication or division by an arbitrary number.

[x ≥ 0 ∧ y > 0]

“Achieve first invariant” ;

[z = y × 2^{n} ∧ n ≥ 0 ∧ x ≥ 0 ∧ y > 0]

while [vrnt: x − z] z ≤ x do “Preserve first invariant” ;

“Achieve second invariant” ;

[x = q × z + r ∧ 0 ≤ r < z ∧ z = y × 2^{n} ∧ n ≥ 0] while [vrnt: n] n ≠ 0 do “Preserve second invariant” [x = q × y + r ∧ 0 ≤ r < y]

Give the verification conditions needed to prove the annotated specification.

An Extension of the Simple Imperative Language

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

⟨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⟩:= ⟨exp⟩ in ⟨comm⟩ | ⟨var⟩:= cons(⟨exp⟩, …, ⟨exp⟩) | ⟨var⟩:= [⟨exp⟩] | [⟨exp⟩] := ⟨exp⟩ | dispose ⟨exp⟩

Why cons and . do not occur in expressions

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

cons(1, 2) = cons(1, 2)

(x = x ∗ y = y)/x → [z], y → [z] is ([z] = [z]) ∗ ([z] = [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 → B
[[−]]_{boolexp} ^{∈} ⟨boolexp⟩ → Stores → B
Γ_{N} = ⟨comm⟩ × States
Γ_{T} = States ∪ {abort}

Transition Rules

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

Conditional and while 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)}

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}

• 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

Pure Commands

A command c is pure if its execution is independent of the heap, i.e.,

∀s, s′ ^{∈} Stores. ∀h, h′ ^{∈} Heaps.
⟨c, (s, h)⟩ ⇝^{∗} (s′, h′) implies h′ = h

and

∀s, s′ ^{∈} Stores. ∀h_{1}, h_{2} ^{∈} Heaps.

(⟨c, (s, h_{1})⟩ ⇝^{∗} abort iff ⟨c, (s, h_{2})⟩ ⇝^{∗} abort)
and (⟨c, (s, h_{1})⟩ ↑ iff ⟨c, (s, h_{2})⟩ ↑)

and (⟨c, (s, h_{1})⟩ ⇝^{∗} (s′, h_{1}) iff ⟨c, (s, h_{2})⟩ ⇝^{∗} (s′, h_{2})).

A command is syntactically 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 syntactically pure command is pure.

An Extension of Assertions

⟨assert⟩ ::= true | false | ⟨exp⟩ = ⟨exp⟩ | ⟨exp⟩ ≠ ⟨exp⟩ | ⋯ | ¬ ⟨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⟩ → States → B

[[true]]_{assert}(s, h) = true,
[[false]]_{assert}(s, h) = false,
[[e_{0} = e_{1}]]_{assert}(s, h) = ([[e_{0}]]_{exp}s = [[e_{1}]]_{exp}s)

(and similarly for ≠, …),

[[ ¬ p]]_{assert}(s, h) = ¬[[p]]_{assert}(s, h),
[[p_{0} ∧ p_{1}]]_{assert}(s, h) = [[p_{0}]]_{assert}(s, h) ∧ [[p_{1}]]_{assert}(s, h)

(and similarly for ∨, ⇒, ⇔),

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

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 p is pure if its meaning is not affected by the heap, i.e., if

∀s ^{∈} Stores. ∃b ^{∈} B. ∀h ^{∈} Heaps. [[p]]_{assert}(s, h) = b.

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

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

Axiom Schemata for ∗

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} ⇒ 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_{1} ∨ p_{2}) ∗ q ⇔ (p_{1} ∗ q) ∨ (p_{2} ∗ q)
(p_{1} ∧ p_{2}) ∗ q ⇒ (p_{1} ∗ q) ∧ (p_{2} ∗ q)
(p ∧ q) ∗ r ⇔ (p ∗ r) ∧ q when q is pure
(∃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}.

An Inference Rule

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

Axiom Schemata for ↦

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

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]

Axiom Schemata for −∗

(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

Inference Rules

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

Derived Inference Rules

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

\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′).

\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} ^{∈} ⟨spec⟩ → B.

[[{p} c {q}]]_{spec} iff ∀σ ^{∈} States. [[p]]_{assert}σ implies ¬ c, σ ⇝^{∗} abort and (∀σ′. c, σ ⇝^{∗} σ′ implies [[q]]_{assert}σ′)

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

Inference Rules for Mutation

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

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

Inference Rules for Construction

For any phrase p, we write p′ for the substitution p/v → v′.

1.

{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. 2.

{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.

3.

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

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

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 (Constancy Revisited)

\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.

Exercise 4.1

None of the following axiom schemata are sound. For each, given an instance which is not valid.

p_{1} ∧ p_{2} ⇏ p_{1} ∗ p_{2}
p_{1} ∗ p_{2} ⇏ p_{1} ∧ p_{2}
(p_{1} ∗ q) ∧ (p_{2} ∗ q) ⇏ (p_{1} ∧ p_{2}) ∗ q
(p_{1} ∨ q) ∗ (p_{2} ∨ q) ⇏ (p_{1} ∗ p_{2}) ∨ q
(p_{1} ∗ p_{2}) ∨ q ⇏ (p_{1} ∨ q) ∗ (p_{2} ∨ q)
(p_{1} ∧ q) ∗ (p_{2} ∧ q) ⇏ (p_{1} ∗ p_{2}) ∧ q
(p_{1} ∗ p_{2}) ∧ q ⇏ (p_{1} ∧ q) ∗ (p_{2} ∧ q)
(p_{1} ⇒ p_{2}) ⇏ (p_{1} ∗ q) ⇒ (p_{2} ∗ q)
∀x. (p_{1} ∗ p_{2}) ⇏ (∀x. p_{1}) ∗ p_{2} when x not free in p_{2}
(p_{1} −∗ p_{2}) ⇏ (p_{1} ⇒ p_{2})
(p_{1} ⇒ p_{2}) ⇏ (p_{1} −∗ p_{2})

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

Exercise 5.1

When

∃α, β. (list α (i, j) ∗ list β (j, k)) ∧ γ = α·β,

we say that j is an interior pointer of the list segment described by list γ (i, k).

1. Give an assertion describing a list segment with two interior pointers j_{1} and j_{2}, such that j_{1} comes before than, or at the same point as, j_{2} in the ordering of the elements of the list segment.

2. Give an assertion describing a list segment with two interior pointers j_{1} and j_{2}, where there is no constraint on the relative positions of j_{1} and j_{2}.

3. Prove that the first assertion implies the second.

Exercise 5.2

A braced list segment is a list segment with an interior pointer j to its last element; in the special case where the list segment is empty, j is nil. Formally,

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

1. Prove the assertion

brlist α (i, j, k) ⇒ list α (i, k).

2. Give an annotated specification of a command that changes the final pointer of a braced list segment from k to l. The command should not construct or deallocate any list structure, and it should not change the value of j. It should satisfy

{brlist α (i, j, k)} ⋯ {brlist α (i, j, l)}.

3. Give an annotated specification of a command that concatenates two braced list segments. The command should not construct or deallocate any list structure, and it should not change the value of k_{2}. It should satisfy

{brlist α (i_{1}, j_{1}, k_{1}) ∗ brlist β (i_{2}, j_{2}, k_{2})}
⋯
{brlist α·β (i_{1}, j, k_{2})}.

Exercise 5.2 (continued)

4. Give an annotated specification of a command that appends an item a at the beginning of a braced list segment. The command should not change the value of k, and should satisfy

{brlist α (i, j, k)} ⋯ {brlist a·α (i, j, k)}.

5. Give an annotated specification of a command that appends an item a at the end of a braced list segment. The command should not change the value of k, and should satisfy

{brlist α (i, j, k)} ⋯ {brlist α·a (i, j, k)}.

6. Give an annotated specification of a command that deletes an item a from the beginning of a nonempty braced list segment. The command should not change the value of k, and should satisfy

{brlist a·α (i, j, k)} ⋯ {brlist α (i, j, k)}.

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

An Alternative Intuitionistic Logic

• We drop the assertion emptyheap.

• We drop the assertion ↦, and make ↪ primitive.

• We alter the definitions of ¬, ⇒, and ⇔. [[e ↪ e′]]_{assert}(s, h)

iff [[e]]_{exp}s ^{∈} dom h and h([[e]]_{exp}s) = [[e′]]_{exp}s, [[ ¬ p]]_{assert}(s, h)

iff ∀h′. h ⊆ h′ ⇒ ¬[[p]]_{assert}(s, h′), [[p_{0} ⇒ p_{1}]]_{assert}(s, h)

iff ∀h′. h ⊆ h′ ⇒ [[p_{0}]]_{assert}(s, h′) ⇒ [[p_{1}]]_{assert}(s, h′), [[p_{0} ⇔ p_{1}]]_{assert}(s, h)

iff [[p_{0} ⇒ p_{1}]]_{assert}(s, h) and [[p_{1} ⇒ p_{0}]]_{assert}(s, h).

The Advantage: Monotonicity

h ⊆ h′ and [[p]]_{assert}(s, h) implies [[p]]_{assert}(s, h′). The Disadvantage: Failure of the Law of the Excluded Middle

x ↪ 13 ∨ (¬ x ↪ 13) fails when h = [y : 14].

A Problematic Specification

{¬(∃x. x → 1, 2)} y := cons(1, 2) {(¬(∃x. x → 1, 2)) ∗ y → 1, 2}.

Translating from Intuitionistic to Classical Semantics

The translation (−)^{o}, from intuitionistic to classical assertions, sends

e ↪ e′ to e ↦ e′ ∗ true
¬ p to true −∗ (¬ p^{o})
p ⇒ q to true −∗ (p^{o} ⇒ q^{o})
p ⇔ q to true −∗ (p^{o} ⇔ q^{o}),

and everything else (inductively) to itself.

Future Directions

• Trees and other abstract data types

• Directed graphs

• Weakest preconditions, dynamic logic, and reference calculi

• Array allocation

• Assertions versus types

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

• Higher-order programming (code pointers)

Answer 1.1

1.

∃x. x > 0 ∧ x < 2

2.

∀x. ∀y. x > 0 ∧ x < 2 ∧ y > 0 ∧ y < 2 ⇒ x = y

3.

∃x ∃y. x > 0 ∧ x < 3 ∧ y > 0 ∧ y < 3 ∧ x ≠ y

4.

∀x. ∀y. ∀z. x > 0 ∧ x < 3 ∧ y > 0 ∧ y < 3 ∧ z > 0 ∧ z < 3

⇒ (x = y ∨ y = z ∨ z = x)

1.

∃x. a × x = b

2.

(∃x. a × x = b) ∧ (∃y. a × y = c)

3.

(∃x. a × x = b) ∧ (∃y. a × y = c)

∧ ((∃x. a′ × x = b) ∧ ∀a′. (∃y. a′ × y = c)) ⇒ a ≥ a′

4.

∀d. 1 < d ∧ d < p ⇒ ¬ (∃x. d × x = p)

Answer 1.2

1.

⟨exp⟩ ::= sum ⟨var⟩ : ⟨exp⟩ to ⟨exp⟩. ⟨exp⟩

2.

[[sum v : e_{0} to e_{1}. e_{2}]]_{exp}σ = ∑_{i=[[e_{0}]]_{exp}σ}^{[[e_{1}]]_{exp}σ}[[e_{2}]]_{exp}[ σ | v: i]

3. The first occurrence of v in sum v : e_{0} to e_{1}. e_{2} is a binder whose scope is e_{2}.

4.

e_{0} > e_{1} ⇒ sum v : e_{0} to e_{1}. e_{2} = 0
e_{0} ≤ e_{1} ⇒ sum v : e_{0} to e_{1}. e_{2}
= (sum v : e_{0} to e_{1} − 1. e_{2}) + (e_{2}/v → e_{1})

e_{0} = e_{1} ⇒ sum v : e_{0} to e_{1}. e_{2} = (e_{2}/v → e_{0}) e_{0} ≤ e_{1} ∧ e_{1} ≤ e_{2} + 1 ⇒ sum v : e_{0} to e_{2}. e_{3}

= (sum v : e_{0} to e_{1} − 1. e_{3}) + (sum v : e_{1} to e_{2}. e_{3})

Answer 2.1

⟨while x ≠ 0 do if x = 1 then skip else x := x − 2, [x : 2]⟩ ⇝ ⟨if x = 1 then skip else x := x − 2 ;

while x ≠ 0 do if x = 1 then skip else x := x − 2, [x : 2]⟩ ⇝ ⟨x := x − 2 ;

while x ≠ 0 do if x = 1 then skip else x := x − 2, [x : 2]⟩ ⇝ ⟨while x ≠ 0 do if x = 1 then skip else x := x − 2, [x : 0]⟩ ⇝ [x : 0]

By the second rule for conditional commands: ⟨if x = 1 then skip else x := x − 2, [x : 2]⟩ ⇝ ⟨x := x − 2, [x : 2]⟩ Then, by the second rule for sequencing: ⟨if x = 1 then skip else x := x − 2 ;

while x ≠ 0 do if x = 1 then skip else x := x − 2, [x : 2]⟩ ⇝ ⟨x := x − 2 ;

while x ≠ 0 do if x = 1 then skip else x := x − 2, [x : 2]⟩

Answer 2.2: The repeat Command

⟨comm⟩ ::= repeat ⟨comm⟩ until ⟨boolexp⟩

Semantics

⟨repeat c until b, σ⟩ ⇝ ⟨c; while ¬ b do c, σ⟩ or

\frac{⟨c, σ⟩ ⇝ ⟨c′, σ′⟩}{⟨repeat c until b, σ⟩ ⇝ ⟨c′ ; while ¬ b do c, σ′⟩}

\frac{⟨c, σ⟩ ⇝ σ′}{⟨repeat c until b, σ⟩ ⇝ ⟨while ¬ b do c, σ′⟩}

or

⟨repeat c until b, σ⟩

⇝ ⟨c; if b then skip else repeat c until b, σ⟩

or \frac{⟨c, σ⟩ ⇝ ⟨c′, σ′⟩}{⟨repeat c until b, σ⟩ ⇝ ⟨c′ ; if b then skip else repeat c until b, σ′⟩}

\frac{⟨c, σ⟩ ⇝ σ′}{⟨repeat c until b, σ⟩ ⇝ ⟨if b then skip else repeat c until b, σ′⟩}

Answer 3.1

[ y = x^{2} ] x := x + 1 ; y := y + 2 × x − 1 [ y = x^{2} ] [y = z ∧ x = w] x := x + y ; y := x − y ; x := x − y [x = z ∧ y = w] [y = x × a ∧ a ≤ b ∨ y = x × b ∧ a ≥ b] while a < b do (a := a + 1 ; y := x + y) [y = x × b] {true} while true do skip {false} [ false ] while true do skip [ false ]

Answer 3.2: Logarithmic-Time Multiplication

[y ≥ 0] z := 0 ; w := x ; k := y ; [z + w × k = x × y ∧ k ≥ 0] while [vrnt: k] k ≠ 0 do

if even k then (k := k ÷ 2 ; w := w + w)

else (k := k − 1 ; z := z + w) [z = x × y]

The verification conditions are:

y ≥ 0 ⇒ (0 + x × y = x × y ∧ y ≥ 0)

(z + w × k = x × y ∧ k ≥ 0 ∧ k ≠ 0 ∧ k = k_{0} ∧ even k) ⇒ (z + (w + w) × (k ÷ 2) = x × y ∧ k ÷ 2 ≥ 0 ∧ k ÷ 2 < k_{0})

(z + w × k = x × y ∧ k ≥ 0 ∧ k ≠ 0 ∧ k = k_{0} ∧ ¬ even k) ⇒ ((z + w) + w × (k − 1) = x × y ∧ k − 1 ≥ 0 ∧ k − 1 < k_{0})

(z + w × k = x × y ∧ k ≥ 0 ∧ k ≠ 0) ⇒ k ≥ 0

(z + w × k = x × y ∧ k ≥ 0 ∧ ¬ k ≠ 0) ⇒ z = x × y

Answer 3.3: Logarithmic-Time Division

[x ≥ 0 ∧ y > 0] n := 0 ; z := y ; [z = y × 2^{n} ∧ n ≥ 0 ∧ x ≥ 0 ∧ y > 0] while [vrnt: x − z] z ≤ x do (n := n + 1 ; z = z × 2) ; q := 0 ; r := x ; [x = q × z + r ∧ 0 ≤ r < z ∧ z = y × 2^{n} ∧ n ≥ 0] while [vrnt: n] n ≠ 0 do

(n := n − 1 ; z := z ÷ 2 ; q := q × 2 ;

[x = q × z + r ∧ 0 ≤ r < z × 2 ∧ z = y × 2^{n} ∧ n ≥ 0 ∧ n < n_{0}] if z ≤ r then q := q + 1 ; r := r − z else skip)

[x = q × y + r ∧ 0 ≤ r < y]

Let

I_{1} =^{def} z = y × 2^{n} ∧ n ≥ 0 ∧ x ≥ 0 ∧ y > 0

I_{2} =^{def} x = q × z + r ∧ 0 ≤ r < z ∧ z = y × 2^{n} ∧ n ≥ 0.

Answer 3.3: Logarithmic-Time Division (continued)

Then the verification conditions are (x ≥ 0 ∧ y > 0) ⇒ (y = y × 2^{0} ∧ 0 ≥ 0 ∧ x ≥ 0 ∧ y > 0) (I_{1} ∧ z ≤ x ∧ x − z = k_{0}) ⇒

(z×2 = y ×2^{n+1} ∧n+1 ≥ 0∧x ≥ 0∧y > 0∧x−z×2 < k_{0}) (I_{1} ∧ z ≤ x) ⇒ x − z ≥ 0 (I_{1} ∧ ¬ z ≤ x) ⇒

(x = 0 × z + x ∧ 0 ≤ x < z ∧ z = y × 2^{n} ∧ n ≥ 0) (I_{2} ∧ n ≠ 0 ∧ n = n_{0}) ⇒

(x = (q × 2) × (z ÷ 2) + r ∧ 0 ≤ r < (z ÷ 2) × 2 ∧

z ÷ 2 = y × 2^{n−1} ∧ n − 1 ≥ 0 ∧ n − 1 < n_{0}) (x = q × z + r ∧ 0 ≤ r < z × 2 ∧

z = y × 2^{n} ∧ n ≥ 0 ∧ n < n_{0} ∧ z ≤ r) ⇒ (x = (q + 1) × z + (r − z) ∧ 0 ≤ r − z < z ∧

z = y × 2^{n} ∧ n ≥ 0 ∧ n < n_{0}) (x = q × z + r ∧ 0 ≤ r < z × 2 ∧

z = y × 2^{n} ∧ n ≥ 0 ∧ n < n_{0} ∧ ¬ z ≤ r) ⇒ (I_{2} ∧ n < n_{0})

(I_{2} ∧ n ≠ 0) ⇒ n ≥ 0 (I_{2} ∧ ¬ n ≠ 0) ⇒ (x = q × y + r ∧ 0 ≤ r < y)

Answers 4.1

p_{1} ∧ p_{2} ⇏ p_{1} ∗ p_{2}  p_{1} : x ↦ 1
p_{2} : x ↦ 1

[sx : 1]

p_{1} ∗ p_{2} ⇏ p_{1} ∧ p_{2}  p_{1} : x ↦ 1
p_{2} : true

[sx : 1, sy : 2]

(p_{1} ∗ q) ∧ (p_{2} ∗ q) ⇏ (p_{1} ∧ p_{2}) ∗ q  p_{1} : x ↦ 1
p_{2} : y ↦ 2

q: x ↦ 1 ∨ y ↦ 2

[sx : 1, sy : 2]

(p_{1} ∨ q) ∗ (p_{2} ∨ q) ⇏ (p_{1} ∗ p_{2}) ∨ q  p_{1} : x ↦ 1
p_{2} : x ↦ 1
q: y ↦ 2

[sx : 1, sy : 2]

(p_{1} ∗ p_{2}) ∨ q ⇏ (p_{1} ∨ q) ∗ (p_{2} ∨ q)  p_{1} : x ↦ 1
p_{2} : x ↦ 1
q: x ↦ 1

[sx : 1]

Answers 4.1 (continued)

(p_{1} ∧ q) ∗ (p_{2} ∧ q) ⇏ (p_{1} ∗ p_{2}) ∧ q  p_{1} : x ↦ 1
p_{2} : y ↦ 2

q: x ↦ 1 ∨ y ↦ 2

[sx : 1, sy : 2]

(p_{1} ∗ p_{2}) ∧ q ⇏ (p_{1} ∧ q) ∗ (p_{2} ∧ q)  p_{1} : x ↦ 1
p_{2} : y ↦ 2

q: x ↦ 1 ∗ y ↦ 2

[sx : 1, sy : 2]

(p_{1} ⇒ p_{2}) ⇏ (p_{1} ∗ q) ⇒ (p_{2} ∗ q)

p_{1} : x ↦ 1 ∨ (x ↦ 1 ∗ y ↦ 2)

p_{2} : true ∗ y ↦ 2

q: y ↦ 2

[sx : 1, sy : 2]

∀x. (p_{1} ∗ p_{2}) ⇏ (∀x. p_{1}) ∗ p_{2} when x not free in p_{2}

p_{1} : if x = 0 then y ↦ 1 else z ↦ 2

p_{2} : y ↦ 1 ∨ z ↦ 2 [sy : 1, sz : 2]

Answers 4.1 (continued)

(p_{1} −∗ p_{2}) ⇏ (p_{1} ⇒ p_{2})  p_{1} : y ↦ 1
p_{2} : x ≠ y

[sy : 1]

(p_{1} ⇒ p_{2}) ⇏ (p_{1} −∗ p_{2})  p_{1} : true
p_{2} : x ↦ 1

[sx : 1]

or p_{1} : x ↦ 1
p_{2} : false

[ ]

Answer 5.1

1.

∃α, β, δ. (list α (i, j_{1}) ∗ list β (j_{1}, j_{2}) ∗ list δ (j_{2}, k))

∧ γ = α·β·δ

2.

(∃α, β. (list α (i, j_{1}) ∗ list β (j_{1}, k)) ∧ γ = α·β)

∧ (∃α, β. (list α (i, j_{2}) ∗ list β (j_{2}, k)) ∧ γ = α·β)

3.

∃α, β, δ. (list α (i, j_{1}) ∗ list β (j_{1}, j_{2}) ∗ list δ (j_{2}, k))

∧ γ = α·β·δ ⇒ (∃α, β, δ. (list α (i, j_{1}) ∗ (list β (j_{1}, j_{2}) ∗ list δ (j_{2}, k)))

∧ γ = α·β·δ) ∧ (∃α, β, δ. ((list α (i, j_{1}) ∗ list β (j_{1}, j_{2})) ∗ list δ (j_{2}, k))

∧ γ = α·β·δ) ⇒ (∃α, β, δ. (list α (i, j_{1}) ∗ list β·δ (j_{1}, k)) ∧ γ = α·β·δ) ∧ (∃α, β, δ. (list α·β (i, j_{2}) ∗ list δ (j_{2}, k)) ∧ γ = α·β·δ) ⇒ (∃α, β. (list α (i, j_{1}) ∗ list β (j_{1}, k)) ∧ γ = α·β)

∧ (∃α, β. (list α (i, j_{2}) ∗ list β (j_{2}, k)) ∧ γ = α·β)

Answer 5.2.1

There are two cases, depending upon whether α is empty:

brlist ϵ (i, j, k)

⇒ emptyheap ∧ i = k ⇒ list ϵ (i, k)

brlist α′·a (i, j, k) ⇒ list α′ (i, j) ∗ j ↦ a, k ⇒ ∃j. list α′ (i, j) ∗ j ↦ a, k ⇒ list α′·a (i, k)

Answer 5.2.2

{brlist α (i, j, k)} if j = nil then

{brlist ϵ (i, j, k) ∧ α = ϵ} {j = nil ∧ emptyheap ∧ α = ϵ} i := l {j = nil ∧ emptyheap ∧ i = l ∧ α = ϵ}

else {∃α′, a. brlist α′·a (i, j, k) ∧ α = α′·a} {∃α′, a. (list α′ (i, j) ∗ j ↦ a, k) ∧ α = α′·a} [j + 1] := l {∃α′, a. (list α′ (i, j) ∗ j ↦ a, l) ∧ α = α′·a}

{brlist α (i, j, l)}

Answer 5.2.3

{brlist α (i_{1}, j_{1}, k_{1}) ∗ brlist β (i_{2}, j_{2}, k_{2})} if j_{1} = nil then i_{1} := i_{2} else [j_{1} + 1] := i_{2} ; {brlist α (i_{1}, j_{1}, i_{2}) ∗ brlist β (i_{2}, j_{2}, k_{2})} if j_{2} = nil then

{brlist α (i_{1}, j_{1}, i_{2}) ∧ β = ϵ ∧ i_{2} = k_{2}} {brlist α·β (i_{1}, j_{1}, k_{2})} j := j_{1}

else {∃β′, b. (brlist α (i_{1}, j_{1}, i_{2}) ∗ brlist β′·b (i_{2}, j_{2}, k_{2})) ∧ β = β′·b} {∃β′, b. (list α (i_{1}, i_{2}) ∗ list β′ (i_{2}, j_{2}) ∗ j_{2} ↦ b, k_{2}) ∧ β = β′·b} {∃β′, b. (list α·β′ (i_{1}, j_{2}) ∗ j_{2} ↦ b, k_{2}) ∧ β = β′·b} {brlist α·β (i_{1}, j_{2}, k_{2})} j := j_{2}

{brlist α·β (i_{1}, j, k_{2})}

Answer 5.2.4

{brlist α (i, j, k)} if j = nil then

{emptyheap ∧ α = ϵ} i := cons(a, k) ; {(emptyheap ∗ i ↦ a, k) ∧ α = ϵ} j := i {(emptyheap ∗ j ↦ a, k) ∧ i = j ∧ α = ϵ} {(list ϵ (i, j) ∗ j ↦ a, k) ∧ α = ϵ} {brlist ϵ·a (i, j, k) ∧ α = ϵ} {brlist a·ϵ (i, j, k) ∧ α = ϵ}

else {∃β, b. brlist β·b (i, j, k) ∧ α = β·b} {∃β, b. (list β (i, j) ∗ j ↦ b, k) ∧ α = β·b} i := cons(a, i) {∃β, b, i′. (i ↦ a, i′ ∗ list β (i′, j) ∗ j ↦ b, k) ∧ α = β·b} {∃β, b. (list a·β (i, j) ∗ j ↦ b, k) ∧ α = β·b} {∃β, b. brlist a·β·b (i, j, k) ∧ α = β·b}

{brlist a·α (i, j, k)}

Answer 5.2.5

{brlist α (i, j, k)} if j = nil then

{emptyheap ∧ α = ϵ} i := cons(a, k) ; {(emptyheap ∧ α = ϵ) ∗ i ↦ a, k} {list α (i, i) ∗ i ↦ a, k} {brlist α·a (i, i, k)} j := i

else {∃β, b. brlist β·b (i, j, k) ∧ α = β·b} {∃β, b. (list β (i, j) ∗ j ↦ b, k) ∧ α = β·b} l := cons(a, k) ; {∃β, b. (list β (i, j) ∗ j ↦ b, k ∗ l ↦ a, k) ∧ α = β·b} [j + 1] := l ; {∃β, b. (list β (i, j) ∗ j ↦ b, l ∗ l ↦ a, k) ∧ α = β·b} {list α (i, l) ∗ l ↦ a, k} {brlist α·a (i, l, k)} j := l

{brlist α·a (i, j, k)}

Answer 5.2.6

{brlist a·α (i, j, k)} {∃β, b. (list β (i, j) ∗ j ↦ b, k) ∧ a·α = β·b} if i = j then

{∃β, b. j ↦ b, k ∧ a·α = β·b ∧ β = ϵ} { j ↦ a, k ∧ α = ϵ} dispose j ; dispose j + 1 ; {emptyheap ∧ α = ϵ} i := k ; j := nil {emptyheap ∧ i = k ∧ j = nil ∧ α = ϵ} {brlist ϵ (i, j, k) ∧ α = ϵ}

else {∃β′, b, l. (i ↦ a, l ∗ list β′ (l, j) ∗ j ↦ b, k) ∧ a·α = a·β′·b} {∃l. i ↦ a, l ∗ brlist α (l, j, k)} l := [i + 1] ; {i ↦ a, l ∗ brlist α (l, j, k)} dispose i ; dispose i + 1 ; {brlist α (l, j, k)} i := l

{brlist α (i, j, k)}