COMP340-08B Lecture Notes

David Goodwin September 20, 2008

This document was produced using L^{A}TEX and typeset with TEX. Fonts are by METAFONT and AMS-L^{A}TEX.

All complaints, comments, corrections and suggestions to David Goodwin (Email: dgsoftnz@gmail.com).

Contents

1 Introduction  5
1.1 Advantages of Formal Methods . . . . . . . . . . . . . . . . . . . 5
1.2 State Vector . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.3 Most basic code . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.4 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.4.1 Example 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.4.2 Example 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
2 Pieces of Code  7
2.1 Assignment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.2 Concatentation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.3 If-then-else . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.4 While . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.4.1 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
2.5 Code . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
2.5.1 Example One . . . . . . . . . . . . . . . . . . . . . . . . . 8
2.5.2 Example Two . . . . . . . . . . . . . . . . . . . . . . . . . 8
3 Floyd-Hoare Logic  11
3.1 Hoare Tripple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
3.1.1 Example One . . . . . . . . . . . . . . . . . . . . . . . . . 11
3.1.2 Example Two . . . . . . . . . . . . . . . . . . . . . . . . . 11
3.1.3 Example Three . . . . . . . . . . . . . . . . . . . . . . . . 11
3.2 Assignment Rule . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
3.2.1 Example One . . . . . . . . . . . . . . . . . . . . . . . . . 12
3.2.2 Example Two . . . . . . . . . . . . . . . . . . . . . . . . . 12
3.2.3 Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
3.3 Weakening Rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
3.3.1 Rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
3.3.2 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
3.4 Concatenation (Composition) Rule . . . . . . . . . . . . . . . . . 13
3.4.1 Proof of Soundness . . . . . . . . . . . . . . . . . . . . . . 13
3.4.2 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
3.5 If-rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
3.6 While Rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
A Lecture Date Map  15

B Lecture Start Notes  17
B.1 9 September 2008 . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
B.2 10 September 2008 . . . . . . . . . . . . . . . . . . . . . . . . . . 17
B.2.1 Revision . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
B.3 11 September 2008 . . . . . . . . . . . . . . . . . . . . . . . . . . 17
B.4 16 September 2008 . . . . . . . . . . . . . . . . . . . . . . . . . . 18
B.5 17 September 2008 . . . . . . . . . . . . . . . . . . . . . . . . . . 18
B.6 18 September 2008 . . . . . . . . . . . . . . . . . . . . . . . . . . 18
C Rigorous Proof of Assignment Rule  19
C.1 Proof One . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
C.2 Proof Two . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

Chapter 1

Introduction

1.1 Advantages of Formal Methods

1. Reduces the need for debugging

2. Forces a clear formulation of program objectives

3. Makes reusing software easier

4. Commercial imperatives The subset of our analysis are \underline{Pieces of Code} - a self contained program (here

written as pseudo-code), which acts as a \underline{function} on its inputs. We assume this pseudo-code is made up of:

1. Usual arithmetic operators and library functions (eg +, ∗, etc)

2. \underline{if-then} and \underline{if-then-else} constructs

3. The \underline{while} construct Note:

• No type declarations (use context)

• No input/output statements

1.2 State Vector

We assume a piece of code acts on a finite set of variables x_{1}, x_{2}, ..., x_{n} (which may be numeric, Boolean, etc). We call (x_{1}, x_{2}, ..., x_{n}) the \underline{Program State}: it is transformed (many times usually) as the program runs. The x_{i} represent \underline{all} variables used in the program.

Suppose x_{i} takes values from the dataset X_{i}, so the state is a “vector” in X_{1} x X_{2} x ... X_{n}.

1.3 Most basic code

The most basic piece of code is an \underline{assignment}, eg x := 3. For this “atomic program”, th state space as only one component, X (= ℕ say). All inputs give output.

1.4 Examples

1.4.1 Example 1

y := x

Here the state space might be ℕxℕIf the input state vector is (x, y) = (2, 3), then the output vector is (2, 2).

To build up more complicated programs we need to use \underline{conditions} or \underline{tests}. These are predicates on the state space (assumed to be of some easily computed form).

1.4.2 Example 2

The test (x < y) on the state space ℕxℕgives the answer \underline{true} if (x, y) = (2, 3) and \underline{false} if (x, y) = (4, 4), etc. We assume such tests are part of the language for building programs. Being predicates, all the usual logical connectives can be applied to them.

Pieces of Code

Fix the state space X = X_{1} x X_{2} x ... X_{n}. Then we can recursively define more complex programs as follows:

2.1 Assignment

As we have seen, assignment statements are pieces of code.

2.2 Concatentation

If P_{1} and P_{2} are two pieces of code, so is P_{1}; P_{2}, \underline{the concatentation} (\underline{composition}) of P_{1} with P_{2}. This is “first P_{1}, then P_{2}”, which obviously corresponds to the composition of functions.

2.3 If-then-else

If P_{1} and P_{2} are two pieces of code, and γ is a \underline{test} on their state space, then

\underline{if}(α) \underline{then} \{P_{1}\} else P_{2}

this is a piece of code.

2.4 While

if α is a test and P a piece of code (both on X), then while(α) {P } is a piece of code. We call P the “body of the loop”. Given input state \underline{x}, the output is obtained by applying P until α is no longer satisfied, the answer is the value of \underline{x} at the point where this occurs (which may be immediately!)

Note: while(α) {P } may not terminate for some input states: The “exit condition” ¬α may never be achieved

2.4.1 Example

Let P = “while(x ≥ 1) {x := x + 1}”. If the input is x ≥ 1 then x is increased each time the body of the loop is applied so the exit condition ¬(x ≥ 1) ⇔ (x < 1) is never satisfied. For example, if x = 1 initially, then the vector (1) evolves as follows:

(1), (2), (3), (4), ...

and does not stop. So P is not defined when x ≥ 1. For x < 1, the entry condition is never satisfied so the output is x: (x), (x)

2.5 Code

Generally, we must think of pieces of code only as partial functions X → X, whose domains generally can’t be determined (by the \underline{Halting Problem}).

2.5.1 Example One

let X_{1} = X_{2} = X_{3} = {0, 1}∗ (all binary strings (*)). Let P = “h := a; a := b; b := h”. The state vector generally is (h, a, b) ∈ X = x_{1} x x_{2} x x_{3} Supose input vector is x = (110, 01, 1001).

before:  code: after:
(110, 01, 1001) h := a (01, 01, 1001)
(01, 01, 1001)  a := b (01, 1001, 1001)
(01, 1001, 1001) b := h (01, 1001, 01)

Generally, if the input vector is (p, q, r), then the output is determined via: (p, q, r) ↦ (q, q, r) ↦ (q, r, r) ↦ (q, r, q) so the second and third positions are swapped, and the value originally in the first position is lost.

2.5.2 Example Two

Suppose code is:

p:=1;i:=1
while(i =< n)
    {p:=p*i;
    i:=i+1}

Suppose the state space is ℕxℕxℕ, with (p, i, n) a typical state. If input is (p_{0}, i_{0}, 4), where p_{0}, i_{0} are any “default values”, we get:

(p_{0}, i_{0}, 4) ↦ (1, i_{0}, 4) ↦ (1, 1, 4)  (2.1)
↦ (1, 1, 4) ↦ (2, 2, 4)  (2.2)
↦ (1, 2, 4) ↦ (2, 3, 4)  (2.3)
↦ (6, 3, 4) ↦ (6, 4, 4)  (2.4)
↦ (24, 4, 4) ↦ (24, 5, 4)  (2.5)

where 2.1 is after two assignments, 2.2 is after one loop, 2.3 is after two loops, 2.4 is after three loops and 2.5 is the output state after the exit condition is satisfied.

2.5. CODE 9

This piece of code \underline{seems} to compute p = n!. How to proive this? How to assert it even?

10 CHAPTER 2. PIECES OF CODE

Floyd-Hoare Logic

3.1 Hoare Tripple

A \underline{Hoare tripple} is a statement ⟨α⟩ P ⟨β⟩ where α, β are tests on the state space X and P a program (= piece of code) acting on X. We say the tripple is \underline{partially correct} if, whenever \underline{x} ∈ Xsatisfiesα, and P is applied to \underline{x}, the result (if it exists) satisfies β. It is \underline{totally correct} if any input \underline{x} satisfying α does give a result when P is applied (P terminates on \underline{x}), and this result satisfies β.

Recalling the factorial program P, it appears that ⟨n ≥ 1⟩ P ⟨P = n!⟩ is both partially and totally correct. Note taht neither (n ≥ 1) nor (p = n!) involves the varible “i”, so its value is not relevant to the correctness.

We call the α, β in ⟨α⟩ P ⟨β⟩ the \underline{precondition} and \underline{postcondition} respectively.

3.1.1 Example One

if X = ℝxℝ, the tripple ⟨y ≠ 0⟩ x := 1/y ⟨x = 1/y⟩ is totally correct where (x, y) ∈ ℝxℝ.

3.1.2 Example Two

⟨ ⟩ a := b ⟨a = b⟩ is totally correct for any choice of state space X_{1}xX_{1}. Here ⟨ ⟩ is called the \underline{empty precondition}, equivalent to ⟨\underline{true}⟩ - it is always satisfied.

3.1.3 Example Three

Pick X = ℤ, the integers.

⟨ ⟩ \underline{while}(P ≥ 1)\{P := P + 1 ⟨P < 1⟩

is partially correct (as if P < 1, the entry condition is not satisfied and if P ≥ 1 it does not terminate). But

⟨P < 1⟩ \underline{while}(P ≥ 1)\{P := P + 1 ⟨P < 1⟩

is totally correct.

3.2 Assignment Rule

The basis of all correctness proofs is provided by the \underline{Assignment Rule}, which states that the following Hoare tripple is (totally) correct:

⟨α[E/x]⟩ x := E ⟨α⟩

Here E is some value, easily computed from the current state variables, either using library functions, or maybe E is a variable or a constant. x is a state variable name, and α[E/x] is the predicate α with x replaced by E where-ever it occurs.

This rule is sound (i.e. does give correct tripples) because if the output to x := E is to satisfy α it is enough that E satisfies the same condition x had to satisfy according to α.

It is also complete (i.e. the precondition is as weak (= general) as possible), so α[E/x] is the \underline{weakest possible precondition} given the piece of code x := E and postcondition ⟨α⟩.

3.2.1 Example One

⟨ ⟩ x := 2 ∗ y ⟨x = 2y⟩

(where x = ℝxℝ) is totally correct, since if we replace x by E = 2y in α = “(x = 2y)′′ gives “(2y = 2y)” which is just \underline{True}

3.2.2 Example Two

⟨x ≤ 0⟩ x := −x ⟨x ≥ 0⟩

is correct, since replacing x by E = −x in (x ≥ 0) gives (−x ≥ 0) which is logically equivalent to (x ≤ 0)

3.2.3 Proofs

See Appendix C for two proofs of the Assignment Rule.

3.3 Weakening Rule

(Precondition strengthening, postcondition weakening)

Suppose ⟨α⟩ P ⟨β⟩ is partially correct. Suppose α_{1} → α is \underline{True} (if α_{1} evaluates to \underline{True} at \underline{x}, so does α), and suppose β → β is \underline{True} . So α_{1} is stronger (or as strong as) α, and β is stronger than (or as strong as) β_{1}. Then also ⟨α_{1}⟩ P ⟨β_{1}⟩ is partially correct.

Proof. Suppose ⟨α⟩ P ⟨β⟩ is partially correct and α_{1} → α and β → β_{1} are both tautologies. Suppose input \underline{x} satisfies α_{1}. Then \underline{x} satisfies α. So when the code P is applied to x, any output satisfies β (since ⟨α⟩ P ⟨β⟩ is partially correct). So any such output satisfies β_{1} (since β → β_{1} is a tautology). So by definition ⟨α⟩ P ⟨β_{1}⟩ is partially corect.

3.3.1 Rule

The weakening rule can be stated as follows:

\frac{α_{1} → α, β → β_{1}, ⟨α⟩ P ⟨β⟩}{⟨α_{1}⟩ P ⟨β_{1}⟩}  (3.1)

3.3.2 Example

The trippe ⟨ ⟩ y := x^{2} ⟨y ≥ 0⟩ is correct by the Assignment Rule (if state space is ℝxℝ), since we get weakest precondition ⟨x^{2} ≥ 0⟩ (=) ⟨ ⟩. Hence so is ⟨x > −10⟩ y := x^{2} ⟨y ≥ −5⟩.

Proof

(x > −10) → \underline{True} , (y ≥ 0) → (y ≥ −5)

is \underline{True} , so we use weakening:

\frac{(x > −10) → true, (y ≥ 0) → (y ≥ −5), ⟨ ⟩ y := x^{2} ⟨y ≥ 0⟩}{⟨x > −10⟩ y := x^{2} ⟨y ≥ −5⟩}

3.4 Concatenation (Composition) Rule

The rule looks like this:

\frac{⟨α⟩ P ⟨β⟩, ⟨β⟩ Q ⟨γ⟩}{⟨α⟩ P; Q ⟨γ⟩}  (3.2)

3.4.1 Proof of Soundness

Assume the hypothesis (are partially correct tripples). Suppose input \underline{x} satisfies α. Apply P to it, then Q. Then after applying P to \underline{x}, any result satisfies β. So wehn Q is applied to that, the result (if any) satisfies γ (by the correctness of ⟨β⟩ Q ⟨γ⟩). So by definition, ⟨α⟩ P; Q ⟨γ⟩ is partially correct.

3.4.2 Example

Prove the following is correct:

⟨ ⟩ c := a + b; c := c/2 ⟨c = (1 + b)/2⟩

(assume a, b, c are Real-valued)

Proof. Work backwards: “feed” the postcondition back through the code. Thus, by assignment rule,

⟨c = a + b⟩(=)⟨c/2 = (a + b)/2⟩ c := c/2 ⟨c = (a + b)/2⟩

But so is:

⟨ ⟩ ⇔ ⟨a + b = a + b⟩ c := a + b ⟨c = a + b⟩

by Assignment. We can now use the \underline{Concatenation Rule}:

\frac{⟨ ⟩ c := a + b ⟨c = a + b⟩, ⟨c = a + b⟩ c := c/2 ⟨c = \frac{a+b}{2}⟩}{⟨ ⟩ c := a + b; c := c/2 ⟨c = \frac{a+b}{2}⟩}

14 CHAPTER 3. FLOYD-HOARE LOGIC Typically we would set out such a proof “Vertically”:

⟨a + b = a + b⟩ ⇔ ⟨ ⟩

c := a + b;

⟨c/2 = \frac{a + b}{2}⟩ ⇔ ⟨c = a + b⟩

c := c/2

⟨c = \frac{a + b}{2}⟩

The method easily extends to arbitrary long concatenations.

3.5 If-rules 3.6 While Rule

Appendix A

Lecture Date Map

This document is a collection notes sorted by topic. This appendix covers which bits of the notes came from which lectures

Date  Content
9 September 2008 chapter 1, The intro to chapter 2 and its sections 2.1, 2.2, 2.3
10 September 2008 Sections 2.4 and 2.5 in chapter 2
11 September 2008 Sections 3.1 and 3.2 in Chapter 3.
16 September 2008 Sections 3.3 and 3.4 in Chapter 3, Appendix C
17 September 2008 Section 3.5 of Chapter 3.
18 September 2008 Section 3.6 of Chapter 3.

16 APPENDIX A. LECTURE DATE MAP

Appendix B

Lecture Start Notes

Notes, announcements and revision content from the beginning of the lectures is not included inline with the notes. It is instead recorded here when present. In the original paper notes, the appropriate section here would come first followed by the content specified in appendix A for the specific date.

B.1 9 September 2008

• Assignments are to be handed in on the third floor of G block under the Mathematics reception counter

• Chapters 4.1, 4.2 and 4.3 of the text book will be covered

• The rest of the paper will cover logical & algebraic methods for reasoning about (the correctness of) programs

B.2 10 September 2008

B.2.1 Revision

if(α) then {P_{1}} else {P_{2}}

is a piece of code. It acts as expected on the state \underline{x}: if α is \underline{true} at \underline{x} then the output agrees with that of P_{1}, otherwise it agrees with P_{2}’s.

Also used is \underline{if-then} without “else”: \underline{if}(α) \underline{then} \{P_{1}\} is a piece of code which, if the input \underline{x} satisfies α, gives the same output as P_{1}, otherwise the output is \underline{x} itself.

Note: the underlining in \underline{x} means its a vector

B.3 11 September 2008

The tutorial is now in K.G.06.

18 APPENDIX B. LECTURE START NOTES

B.4 16 September 2008

A copy of two hand-written rigorous proofs of the Assignment Rule were handed out. See Appendix C sections C.1 and C.2.

B.5 17 September 2008

No pre-content notes were recorded for this lecture.

B.6 18 September 2008

No pre-content notes were recorded for this lecture.

Appendix C

Rigorous Proof of Assignment Rule

Note: This was copied from a photocopy of handwritten text. Difficulties in reading such text can result in copy errors.

C.1 Proof One

Proof.

⟨α[E/x]⟩ x := E ⟨α⟩  (C.1)

Say state variables are x_{1}, x_{2}, …, x_{n}, x_{i} ∈ X_{i} (without loss of generality). Now suppose assignment is x_{1} := E(x_{1}, x_{2}, …, x_{n}) (wlog). Let:

β(x_{1}, …, x_{n}) = α[E(x_{1}, …, x_{n}), x_{2}, …, x_{n}]
= α[E/x_{1}]

another predicate.

Suppose an input state vector (a_{1}, a_{2}, …, a_{n}) satisfies β, so α(E(a_{1}, a_{2}, …, a_{n}), a_{2}, …, a_{n}) satisfies β, so α(E(a_{1}, a_{2}, …, a_{n}), a_{2}, …, a_{n}) is \underline{True} . Now set b_{1} = E(a_{1}, a_{2}, …, a_{n}), so output vector is (E(a_{1}, a_{2}, …, a_{n}), a_{2}, …, a_{n}). Then α(b_{1}, a_{2}, …, a_{n}) = β(a_{1}, a_{2}, …, a_{n}) is \underline{True} . So this shows equation C.1 is \underline{correct}.

Is β = α[E/x_{1}] as general as possible? Need to show any input to the assignment that satisfies the postcondition must also satisfiy the precondition. Put another way, we need to show that if the precondition β is \underline{not} satisfied, nor can the postcondition be.

So say β(a_{1}, a − 2, …, a_{n}) = α(E(a_{1}, a_{2}, …, a_{n}), a_{2}, …, a_{n}) is \underline{False} . Then letting b_{1} = E(a_{1}, a_{2}, …, a_{n}), the output of the assignment given input (a_{1}, a_{2}, …, a_{n}) is (b_{1}, a_{2}, …, a_{n}), and of course α(b_{1}, a_{2}, …, a_{n}) = β(a_{1}, a_{2}, …, a_{n}), which is \underline{False} .

C.2 Proof Two

Proof.

⟨α[E/x]⟩ x := E ⟨α⟩

Suppose the state variables are x_{1}, x_{2}, …, x_{n}. Suppose that the assignment has the form x_{1} := E(x_{1}, x_{2}, …, x_{n}), with no loss of generality.

Define β(x_{1}, x_{2}, …, x_{n}) = α(E(x_{1}, …, x_{n}), x_{2}, …, x_{n}), a test. Then let (a_{1}, a_{2}, …, a_{n}) be a state vector for input.

Following the application of the assignment, the output is

E(a_{1}, a_{2}, …, a_{n}), a_{2}, …, a_{n}) = (b_{1}, a_{2}, …, a_{n})

Clearly then, β(a_{1}, a_{2}, …, a_{n}) = α(b_{1}, a_{2}, …, a_{n}). So (a_{1}, a_{2}, …, a_{n}) satisfies β = α[E/x] if and only if (b_{1}, a_{2}, …, a_{n}) satisfies α

So α[E/x_{1}] counts as \underline{True} every possible input to the assignment that gives an output satisfying α. So β = α[E/x_{1}] is the most general possible precondition making the tripple correct.