xuebaunion@vip.163.com

3551 Trousdale Rkwy, University Park, Los Angeles, CA

留学生论文指导和课程辅导

无忧GPA：https://www.essaygpa.com

工作时间：全年无休-早上8点到凌晨3点

微信客服：xiaoxionga100

微信客服：ITCS521

Propositional Logic代写-COMP1600 /

时间：2022-09-03

Hoare Logic: Total Correctness

COMP1600 / COMP6260

slides created by: Dirk Pattinson

(with contributions by Victor Rivera and previous colleagues)

convenor: Pascal Bercher

lecturer: Michael Norrish

Australian National University

Semester 2, 2022

Recall: Hoare Logic

Basic Ingredient. Hoare-triples

{P} S {Q}

P and Q are predicates (formulae)

S is a code (fragment)

Example. {x > 0} while (x>0) do x := x-1 {x = 0}

Meaning. If we run S from a state that satisfies precondition P and if S

terminates, then the post-state will satisfy Q.

1 / 49

Hoare Logic

Idea. Proof Rules that allow us to prove all true triples.

Assignment

{Q(e)} x := e {Q(x)}

Precondition Strengthening / Postcondition Weakening

Ps → Pw {Pw} S {Q}

{Ps} S {Q}

{P} S {Qs} Qs → Qw

{P} S {Qw}

Sequence.

{P} S1 {Q} {Q} S2 {R}

{P} S1; S2 {R}

Conditional.

{P ∧ b} S1 {Q} {P ∧ ¬b} S2 {Q}

{P} if b then S1 else S2 {Q}

2 / 49

Proof Rule for While Loops (Rule 6/6)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b}

I is called the loop invariant.

I is true before we encounter the while statement, and remains true

each time around the loop (although not necessarily midway during

execution of the loop body).

If the loop terminates the control condition must be false, so ¬b

appears in the postcondition.

For the body of the loop S to execute, b needs to be true, so it

appears in the precondition.

3 / 49

Soundness of the While Rule w.r.t. the semantics

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b}

Soundness. If the premise is true, then so is the conclusion.

assume that I holds in the initial state.

if b is false, nothing happens, so I ∧ ¬b is true in post-state.

if b is true, then (by premise) I holds at end of each iteration

assuming that the loop terminates, b becomes false (and I still holds)

Q. What about non-termination?

4 / 49

Applying the While Rule

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

Difficult bit. Finding the right invariant.

This requires intuition and practice. There is no automated way of

doing this.

Easy bit. Establishing the desired postcondition

The postcondition we get after applying our rule has form I ∧ ¬b.

But if I ∧ ¬b → Q, we can use postcondition weakening.

Easy bit. Establishing the desired precondition

The precondition we get after applying our rule has form I . But if

P → I , we can use precondition strengtening.

5 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2. {I} while b do S {I ∧ ¬b} (While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6. {P} while b do S {Q} (Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2. {I} while b do S {I ∧ ¬b} (While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2.

{I} while b do S {I ∧ ¬b}

(While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1.

{I ∧ b} S {I}

2.

{I} while b do S {I ∧ ¬b}

(While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2.

{I} while b do S {I ∧ ¬b}

(While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2. {I} while b do S {I ∧ ¬b} (While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2. {I} while b do S {I ∧ ¬b} (While Loop, 1)

3.

I ∧ ¬b → Q

(Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2. {I} while b do S {I ∧ ¬b} (While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2. {I} while b do S {I ∧ ¬b} (While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2. {I} while b do S {I ∧ ¬b} (While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5.

P → I

(Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2. {I} while b do S {I ∧ ¬b} (While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2. {I} while b do S {I ∧ ¬b} (While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6. {P} while b do S {Q} (Precondition Strengthening, 4, 6)

6 / 49

Example

Goal. Find condition I to prove that:

{n > 3} while n>0 do n := n-1 {n = 0}

Observation. Need to prove the above using while-rule, i.e.

{I ∧ b} n := n− 1 {I}

{I} while (n>0) do n:= n-1 {I ∧ n ≤ 0}

Want. Loop invariant I such that

It is implied by the precondition:

n > 3→ I

if the loop terminates (i.e. n > 0 is false), then I should imply the

postcondition:

I ∧ n ≤ 0→ n = 0

If I is true and the body is executed, I is true afterwards:

{I ∧ n > 0} n := n− 1 {I}

Loop Invariant. I ≡ (n ≥ 0)

have {n ≥ 0 ∧ n > 0} n := n− 1 {n ≥ 0}

n ≥ 0 ∧ ¬(n > 0)→ n = 0

7 / 49

Example (cont.)

Goal. Find condition I to prove that:

{n > 3} while n>0 do n := n-1 {n = 0}

Loop Invariant. I ≡ (n ≥ 0), we have

n > 3→ n ≥ 0,

n ≥ 0 ∧ n ≤ 0→ n = 0, and

{n ≥ 0 ∧ n > 0} n := n− 1 {n ≥ 0}.

7 / 49

Example, Formally

1. {n − 1 ≥ 0} n := n− 1 {n ≥ 0} (Assignment)

2. n ≥ 0 ∧ n > 0→ n − 1 > 0 (Logic)

3. {n ≥ 0 ∧ n > 0} n := n− 1 {n ≥ 0} (Prec. Strength., 1, 2)

4. {n ≥ 0} while (n > 0) do n := n− 1 {n ≥ 0∧¬(n > 0)} (While Loop, 3)

5. n > 3→ n ≥ 0 (Logic)

6. {n > 3} while (n > 0) do n := n− 1 {n ≥ 0 ∧ ¬(n > 0)} (Prec.

Strength., 4, 5)

7. n = 0↔ n ≥ 0 ∧ ¬(n > 0) (Logic)

8. {n ≥ 0} while (n > 0) do n := n− 1 {n = 0} (Post. Equiv., 6, 7)

Other Invariants

e.g. true or n = 0

both are invariants, and give n = 0 as postcondition

but n ≥ 0 is better (weaker) as it is more general.

8 / 49

Let’s Prove a Program!

Program (with specification):

{True}

i:=0;

s:=0;

while (i ̸= n) do

i:=i+1;

s:=s+(2*i-1)

{s = n2}

(The sum of the first n odd numbers is n2)

Goal: prove

{True} Program {s = n2}

9 / 49

A Very Informal Analysis

Let’s look at some examples:

1 = 1 = 12

1 + 3 = 4 = 22

1 + 3 + 5 = 9 = 32

1 + 3 + 5 + 7 = 16 = 42 . . .

It looks OK - let’s see if we can prove it!

Goal: prove

{True} Program {s = n2}

10 / 49

How can we prove it?

First Task. Find a loop invariant I . (NB: S and s are different!)

Post condition and loop condition:

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b}

while (i ̸= n) do

i:=i+1; (1, 2, 3, ...)

s:=s+(2*i-1) (1, 4, 9, ...)

{s = n2}

Want. (I ∧ i = n)→ (s = n2) to apply postcondweak

Loop Body. Each time i increments, s moves to next square number.

Invariant. I ≡ s = i2.

11 / 49

Check I as (s = i2) is an invariant: prove {I}S{I}

{s = i2} i := i + 1 {Q} {Q} s := s + (2 ∗ i − 1) {s = i2}

Seq{s = i2} i := i + 1; s := s + (2 ∗ i − 1) {s = i2}

Using the assignment axiom and the sequence rule:

1. {Q} s:=s+(2*i-1) {s = i2}

2.

3. {s = i2} i:=i+1 {Q}

4. {s = i2} i:=i+1; s:=s+(2*i-1) {s = i2} (Sequence, 3, 1)

12 / 49

Check I as (s = i2) is an invariant: prove {I}S{I}

{s = i2} i := i + 1 {Q} {Q} s := s + (2 ∗ i − 1) {s = i2}

Seq{s = i2} i := i + 1; s := s + (2 ∗ i − 1) {s = i2}

Q is {s + (2 ∗ i − 1) = i2}

Using the assignment axiom and the sequence rule:

1. {s + (2 ∗ i − 1) = i2} s:=s+(2*i-1) {s = i2} (Assignment)

2.

3. {s = i2} i:=i+1 {s + (2 ∗ i − 1) = i2}

4. {s = i2} i:=i+1; s:=s+(2*i-1) {s = i2} (Sequence, 3, 1)

13 / 49

Check I as (s = i2) is an invariant: prove {I}S{I}

{s = i2} i := i + 1 {Q} {Q} s := s + (2 ∗ i − 1) {s = i2}

Seq{s = i2} i := i + 1; s := s + (2 ∗ i − 1) {s = i2}

Q is {s + (2 ∗ i − 1) = i2}

Using the assignment axiom and the sequence rule:

1. {s + (2 ∗ i − 1) = i2} s:=s+(2*i-1) {s = i2} (Assignment)

2. {s + (2 ∗ (i + 1)− 1) = (i + 1)2} i:=i+1 {s + (2 ∗ i − 1) = i2}

(Assignment)

3. {s = i2} i:=i+1 {s + (2 ∗ i − 1) = i2} (Prec. Equiv., 2)

4. {s = i2} i:=i+1; s:=s+(2*i-1) {s = i2} (Sequence, 3, 1)

So far, so good. (I as (s = i2) is an invariant.)

14 / 49

Completing the Proof of {True} Program {s = n2}

6 Strengthen the precondition to match the While rule premise

{I ∧ b} S {I}

{(s = i2) ∧ (i ̸= n)} i:=i+1; s:=s+(2*i-1) {s = i2}

7 Apply the While rule and postcondition equiv:

s = i2 ∧ i = n↔ s = n2

{s = i2} while ... s:=s+(2*i-1) {s = n2}

8 Check that the initialisation establishes the invariant:

{0 = 02} i:=0 {0 = i2} {0 = i2} s:=0 {s = i2}

{0 = 02} i:=0; s:=0 {s = i2}

9 (0 = 02) ↔ True, so putting it all together with Sequencing we have

{True} i := 0 ; s := 0 ; while (i ̸= n) do S {s = n2}

15 / 49

What about Termination?

Hoare Logic (in this form) proves partial correctness.

Example. while 1+1 = 2 do x:=0.

This will loop forever!

can still prove things about it

Exercise.

{True} while 1+1 = 2 do x:=0 {False}

Termination.

remember functional programs? Something must decrease

need loop variant (later)

16 / 49

Are the Rules Complete?

So far. Have a very simple language

new rules for arrays, for-loops, exceptions, . . .

Focus here. Soundness

every provable Hoare triple is (semantically) true

soundness holds but terms and conditions apply

with these assumptions, also have completeness, i.e. every true Hoare

triple is provable.

Completeness. if {P} S {Q} is true then {P} S {Q} is provable

17 / 49

What are these Assumptions?

The language we use for expressions in our programs is the same as

the language we use in our pre- and postconditions (in our case, basic

arithmetic).

We assumed no aliasing of variables. (In most real languages we can

have multiple names for the one piece of memory.)

How is aliasing a problem?

Suppose x and y refer to the same cell of memory.

▶ We get {y +1 = 5 ∧ y = 5} x:=y+1 {x = 5 ∧ y = 5} (Assignment)

▶ i.e. {y = 4 ∧ y = 5} x:=y+1 {x = 5 ∧ y = 5}

▶ i.e. if initial state satisfies False and x:=y+1 terminates then final state

satisfies {x = 5 ∧ y = 5} (but also works for x = 6 ∧ y = 6)

which makes a mockery of our calculus since it proves rubbish!

18 / 49

What are these Assumptions?

The language we use for expressions in our programs is the same as

the language we use in our pre- and postconditions (in our case, basic

arithmetic).

We assumed no aliasing of variables. (In most real languages we can

have multiple names for the one piece of memory.)

How is aliasing a problem?

Suppose x and y refer to the same cell of memory.

▶ We get {y +1 = 5 ∧ y = 5} x:=y+1 {x = 5 ∧ y = 5} (Assignment)

▶ i.e. {y = 4 ∧ y = 5} x:=y+1 {x = 5 ∧ y = 5}

▶ i.e. if initial state satisfies False and x:=y+1 terminates then final state

satisfies {x = 5 ∧ y = 5} (but also works for x = 6 ∧ y = 6)

which makes a mockery of our calculus since it proves rubbish!

18 / 49

Finding a Proof

Example.

{ n >= 0 }

f := 1;

i := n;

while (i > 0) do

f := f * i;

i := i-1;

{ f = n! }

19 / 49

Finding a Proof

Annotating the program: I = f ∗ i ! = n! ∧ i ≥ 0

{ n >= 0 }

f := 1;

{ f = 1 /\ n >= 0 } -- provable with assignment

i := n;

{ f = 1 /\ i = n /\ n >= 0} -- provable with assignment

==> -- use postcond weakening

{ I } -- general premise of while rule

while (i > 0) do

{ I /\ i > 0 } -- proof obligation for loop body

f := f * i; -- n, n * (n-1), n * (n-1) * (n-2) ...

i := i-1; -- n-1, n-2, n-3, ...

{ I } -- up until here.

{ I /\ not(i > 0) } -- general conclusion of while rule

==> -- use postcond weakening

{ f = n! }

Invariant: f * i! = n! / i >= 0

20 / 49

From Annotated Programs to Proofs

Initialisation Part

{ n >= 0 }

f := 1;

{ f = 1 /\ n >= 0 } -- provable with assignment

i := n;

{ f = 1 /\ i = n /\ n >= 0} -- provable with assignment

1. {f = 1∧ n = n∧ n ≥ 0} i := n {f = 1∧ i = n∧ n ≥ 0} (Assignment)

2. {1 = 1∧n = n∧n ≥ 0} f := 1 {f = 1∧n = n∧n ≥ 0} (Assignment)

3. n ≥ 0↔ 1 = 1 ∧ n = n ∧ n ≥ 0 (Logic)

4. {n ≥ 0} f := 1 {f = 1 ∧ n = n ∧ n ≥ 0} (Prec. Equiv. 2, 3)

5. {n ≥ 0} f := 1; i := n {f = 1 ∧ i = n ∧ n ≥ 0} (Sequence, 1, 4)

21 / 49

From Invariant to Loop Body

{ I } -- general premis of while rule

while (i > 0) do

{ I /\ i > 0 } -- proof obligation for loop body

f := f * i; -- n, n * (n-1), n * (n-1) * (n-2) ...

i := i-1; -- n-1, n-2, n-3, ...

{ I } -- up until here.

{ I /\ not(i > 0) } -- general conclusion of while rule

Invariant. I = f ∗ i ! = n! ∧ i ≥ 0

Loop Body: Proof obligation

{ f * i! = n! /\ i >= 0 /\ i > 0 }

f := f * i;

i := i - 1;

{ f * i! = n! /\ i >= 0}

22 / 49

From Annotated Programs to Proofs

Loop Body

{ f * i! = n! /\ i >= 0 /\ i > 0 } -- proof obligation

for loop body

f := f * i;

{ f * (i-1)! = n! /\ i >= 0 /\ i > 0} -- new annotation!

i := i-1;

{ f * i! = n! /\ i >= 0 } -- end loop body

6. {f ∗ (i − 1)! = n! ∧ (i − 1) ≥ 0} i := i− 1 {f ∗ i! = n! ∧ i ≥ 0}(Assignment)

7. {(f ∗ i) ∗ (i − 1)! = n! ∧ (i − 1) ≥ 0} f := f ∗ i {f ∗ (i − 1)! = n! ∧ (i − 1) ≥ 0} (Assignment)

8. f ∗ i! = n! ∧ i ≥ 0 ∧ i > 0→ (f ∗ i) ∗ (i − 1)! = n! ∧ (i − 1) ≥ 0 (Logic)

9. {f ∗ i! = n! ∧ i ≥ 0 ∧ i > 0} f := f ∗ i {f ∗ (i − 1)! = n! ∧ (i − 1) ≥ 0} (Prec. Stren., 7,8)

10. {f ∗ i! = n! ∧ i ≥ 0 ∧ i > 0} f := f ∗ i; i := i− 1 {f ∗ i! = n! ∧ i ≥ 0} (Sequence, 6,9)

23 / 49

From Annotated Programs to Proofs

Loop Body to While Loop

{ f * i! = n! /\ i >= 0 } -- premise of while

rule: "I"

while (i > 0) do

{ f * i! = n! /\ i >= 0 /\ i > 0 } -- "I /\ b"

f := f * i;

i := i-1;

{ f * i! = n! /\ i >= 0 } -- "I"

{ f * i! = n! /\ i >= 0 /\ not(i > 0) } -- conclusion of while:

"I /\ not b"

11. {f ∗ i ! = n! ∧ i ≥ 0}

while (i > 0) do { f:= f*i; i:= i-1}

{f ∗ i ! = n! ∧ i ≥ 0 ∧ ¬(i > 0)} (While, 10)

24 / 49

Putting it all together

{ n >= 0 }

f := 1;

i := n;

{ f = 1 /\ i = n /\ n >= 0} -- have already

==> -- postcond weakening

{ f * i! = n! /\ i >= 0 }

while (i > 0) do

f := f * i;

i := i-1;

{ f * i! = n! /\ i >= 0 /\ not(i > 0) } -- have already

==> -- postcond weakening

{ f = n! }

12. f = 1 ∧ i = n ∧ n ≥ 0→ f ∗ i ! = n! ∧ i ≥ 0 (Logic)

13. {n ≥ 0} f := 1; i := n {f ∗ i ! = n! ∧ i ≥ 0} (Postcond. Weak., 5, 12)

14. {n ≥ 0} program {f ∗ i ! = n! ∧ i ≥ 0 ∧ ¬(i > 0)} (Seq., 13, 11)

15. f ∗ i ! = n! ∧ i ≥ 0 ∧ ¬(i > 0)→ f = n! (Logic)

16. {n ≥ 0} program {f = n!} (Postcondition Weakening, 14, 15)

25 / 49

Hoare Logic: Total Correctness

Motto. Total Correctness = partial correctness + termination

New Notation.

[P] S [Q]

P and Q are precondition and postcondition, as before

S is a code fragment

Meaning. If the precondition holds, then executing S will terminate, and

the postcondition is true.

Example.

[P] S [true] – S always terminates from precondition P

{P} S {false} – S never terminates from precondition P

26 / 49

Rules for Total Correctness

Q. What are the rules for total correctness?

assignment

sequencing

conditional

pre/post strengthening/weakening

still work, as there’s no danger of non-termination.

Problematic Rule. while (may introduce non-termination)

27 / 49

Assignment, revisited

[Q(e)] x := e [Q(x)]

Assumptions. (fine for our toy language)

evaluation of expression e terminates.

evaluation of e returns a number (no exception e.g.)

In General.

the expression can be recursively defined

there may be errors, e.g. division by zero

28 / 49

Rules for Total Correctness

Ps → Pw [Pw ] S [Q]

[Ps ] S [Q]

(Precondition Strengthening)

[P] S [Qs ] Qs → Qw

[P] S [Qw ]

(Postcondition Weakening)

[P] S1 [Q] [Q] S2 [R]

[P] S1; S2 [R]

(Sequence)

[P ∧ b] S1 [Q] [P ∧ ¬b] S2 [Q]

[P] if b then S1 else S2 [Q]

(Conditional)

Assumption. Evaluation of b always terminates (OK here)

29 / 49

Termination of Loops

Example

[y > 0]

while (y < r) do

r := r - y;

q := q + 1

[true]

30 / 49

Termination of Loops

Example

[y > 0]

while (y < r) do

r := r - y;

q := q + 1

[true]

Observations.

q := q + 1 irrelevant

y doesn’t change, always positive

r strictly decreases in each iteration

y < r will eventually be false.

31 / 49

Termination of Loops: General Condition

Example

[y > 0]

while (y < r) do

r := r - y;

q := q + 1

[true]

Termination follows if we have a variant E that is,

E ≥ 0 at the beginning of each iteration

E strictly decreases at each iteration

Q. What could be a variant in this example?

32 / 49

While Rule for Total Correctness

Goal. Show that

[P] while b do S [Q]

In Addition to partial correctness (e.g. finding I ), find variant E such

that

E ≥ 0 at the beginning of each iteration:

I ∧ b → E ≥ 0

E is strictly decreasing in each iteration

[I ∧ b ∧ (E = n)] S [I ∧ E < n]

where n is an auxiliary variable not appearing elsewhere, to

“remember” initial value of E

33 / 49

While Rule for Total Correctness

I ∧ b → E ≥ 0 [I ∧ b ∧ E = n] S [I ∧ E < n]

[I ] while b do S [I ∧ ¬b]

where n is an auxiliary variable not appearing elsewhere.

Intuition.

E is an upper bound to the number of loop iterations

termination of functional programs: measure decrease in recursive call

34 / 49

Example

Goal. [y > 0] while (y < r) do r := r - y; q := q+1 [true]

Focus. Loop body r := r - y; q := q + 1

want some invariant: let’s just call it I

want some variant: here r is decreasing

First Goal. The variant is ≥ 0 when we enter the loop:

formally: I ∧ (y < r)→ r ≥ 0

this suggests I ≡ y > 0

Second Goal. The invariant is re-established, and the variant decreases

formally:

[(y > 0) ∧ (y < r) ∧ r = n] r := r = y; q:= q+1 [(y > 0) ∧ r < n]

this seems to be right, so let’s prove it!

35 / 49

Example Proof

Goal.

[(y > 0) ∧ (y < r) ∧ r = n] r := r - y; q:= q+1 [(y > 0) ∧ r < n]

First Assignment.

[(y > 0) ∧ (r < n)] q := q+ 1 [y > 0 ∧ r < n]

Second Assignment.

[(y > 0) ∧ (r − y < n)] r := r-y [y > 0 ∧ r < n]

Sequencing.

[(y > 0) ∧ (r − y < n)] r := r-y; q := q+1 [y > 0 ∧ r < n]

Precondition Strengthening.

[(y > 0) ∧ (y < r) ∧ (r = n)] r := r - y; q := q+1 [y > 0 ∧ r < n]

36 / 49

Completing the Proof

While Rule.

I ∧ b → E ≥ 0 [I ∧ b ∧ E = n] S [I ∧ E < n]

[I ] while b do S [I ∧ ¬b]

1. [(y > 0) ∧ (r < n)] q := q+ 1 [y > 0 ∧ r < n] (Assignment)

2. [(y > 0) ∧ (r − y < n)] r := r-y [y > 0 ∧ r < n] (Assignment)

3. [(y > 0) ∧ (r − y < n)] r := r-y; q := q+1 [y > 0 ∧ r < n] (Sequence, 2, 1)

4. (y > 0) ∧ (y < r) ∧ (r = n)→ (y > 0) ∧ (r − y < n) (Logic)

5. [(y > 0) ∧ (y < r) ∧ (r = n)] r := r-y; q := q+1 [y > 0 ∧ r < n] (Prec.

Streng., 2, 3)

6. (y > 0) ∧ (y < r)→ r ≥ 0 (Logic.)

7. [y > 0] while (y < r) do r:= r-y; q:= q+1 [y > 0 ∧ y ≥ r ] (While Loop, 5,

6)

8. y > 0 ∧ y ≥ r → true

9. [y > 0] while (y < r) do r:= r-y; q:= q+1 [true] (Postc. Weak., 7, 8)

37 / 49

Second Example

[n >= 0]

fact := 1;

i := n;

while (i > 0) do

fact := fact * i;

i := i - 1

[fact = n!]

Q1. What is the invariant (linking n, fact and i)?

before: fact = 1, i = n

1st iteration: fact = n, i = n-1

2nd iteration: fact = n * (n-1), i = n-2

...

last iteration: fact = n * ... * 1, i = 0

Invariant: fact ∗ i ! = n!

38 / 49

Second Example

[n >= 0]

fact := 1;

i := n;

while (i > 0) do

fact := fact * i;

i := i - 1

[fact = n!]

Q2. Is the invariant fact ∗ i ! = n! good enough?

true initially: for fact = 1 and i = n.

implies postcondition: fact ∗ i ! = n! ∧ ¬(i > 0)→ fact = n!

Stronger Invariant. fact ∗ i ! = n! ∧ i ≥ 0

39 / 49

Second Example

[n >= 0]

fact := 1;

i := n;

while (i > 0) do

fact := fact * i;

i := i - 1

[fact = n!]

Q3. What’s the variant?

i ≥ 0 for every iteration (I ∧ b → E ≥ 0)

decreases with every iteration

Variant. E ≡ i

40 / 49

Proof Skeleton

Simple Assignments.

[n >= 0]

fact := 1;

i := n;

[n >= 0 /\ fact = 1 /\ i = n]

Applying While

[ fact * i! = n! /\ i >= 0 ]

while (i > 0) do

fact := fact * i;

i := i - 1

[ fact * i! = n! /\ i >= 0 /\ i <= 0]

Missing Glue. Weakening / Strengthening

from postcondition of assignments to precondition of while

from postcondition of while to goal statement (fact = n!)

41 / 49

Zooming in on While

[ fact * i! = n! /\ i >= 0 ]

while (i > 0) do

fact := fact * i;

i := i - 1

[ fact * i! = n! /\ i >= 0 /\ i <= 0]

Loop Body (Invariant: fact ∗ i ! = n! ∧ i ≥ 0, Variant: i)

[fact * i! = n! /\ i >= 0 /\ i > 0 /\ i = a]

fact := fact * i;

i := i - 1

[ fact * i! = n! /\ i >= 0 /\ i < a]

Positivity Condition. fact ∗ i ! = n! ∧ i ≥ 0 ∧ i > 0→ i ≥ 0 (Maths)

42 / 49

While Rule: Soundness

I ∧ b → E ≥ 0 [I ∧ b ∧ E = n] S [I ∧ E < n]

[I ] while b do S [I ∧ ¬b]

Partial Correctness.

premises of the rule imply those of the rule for partial correctness

so if the loop terminates, the postcondition holds

Missing. Termination

43 / 49

Termination Analysis

I ∧ b → E ≥ 0 [I ∧ b ∧ E = n] S [I ∧ E < n]

[I ] while b do S [I ∧ ¬b]

Let σ be a state that validates the precondition I . If b is false in σ, we are

done. Assume that b is true in σ, hence the value of E in σ is ≥ 0.

Induction on the value σ(E ) of E in state σ.

Base case. σ(E ) = 0.

Right premise implies that E < 0 after one iteration

With left premise, get that ¬b after one iteration

hence the loop terminates after one iteration.

Step Case. Let σ(E ) = k + 1

after one iteration, have σ(E ) ≤ k

statement follows by induction hypothesis.

44 / 49

Variation: More Expressive Logic

So far. In triples {P} S {Q} we have

S a program fragment (we keep this for now)

P and Q propositional formulae made from basic arithmetic

Q. How about expressing the following?

{true} x := 2 ∗ x {even(x)}

A. We could say that even(x) = ∃y .2 ∗ y = x

Change. Allowing pre/postconditions to be first order formulae.

45 / 49

Example.

{true} x := 2 ∗ x {∃y .2 ∗ y = x}

Using the assignment axiom.

{∃y .2 ∗ y = 2 ∗ x} x := 2 ∗ x {∃y .2 ∗ y = x}

More Expressive Logic. Assertions are first-order formulae

all rules remain valid

Hoare-logic is (almost) insensitive to underlying logic

46 / 49

Variation: More Expressive Programs

Example Feature. Arrays

allow expressions to contain a[i ]

(we assume that the index is always in scope)

Maximum Finding

m := a[0]

i := 1;

while (i < n) do

if a[i] > m then m := a[i] else m := m;

i := i + 1

Q. How do we express that m is the maximum array element?

A. Use first order logic.

m is largest: ∀k .0 ≤ k < n→ m ≥ a[k]

m is in array: ∃k .0 ≤ k < n ∧m = a[k]

47 / 49

Annotated Code

{n >= 1}

m := a[0]

i := 1;

{m = a[0] /\ i = 1 /\ n >= 1 }

==>

{forall k. 0 <= k < i -> m >= a[k] /\ i <= n}

while (i < n) do

if a[i] > m then m := a[i] else m := m;

i := i + 1

{forall k. 0 <= k < i -> m >= a[k] /\ i <= n /\ i >= n}

==>

{forall k. 0 <= k < n -> m <= a[k]}

Invariant. I ≡ ∀k .0 ≤ k < i → m ≤ a[k] ∧ i ≤ n

initially: m = a[0] ∧ i = 1→ I

at end: I ∧ i ≥ n→ ∀k .0 ≤ k < n→ m ≤ a[i ]

Remark. Can turn this into a formal proof as before.

48 / 49

References

The textbook has material on Hoare Logic

Grassman & Tremblay, “Logic and Discrete Mathematics: A

Computer Science Perspective”, Prentice-Hall, Chapter 9, pp.

481-518.

Some nice online notes with lots of examples:

Gordon, “Specification and Verification I”, http://www.cl.cam.ac.

uk/~mjcg/Lectures/SpecVer1/SpecVer1.html, Chapters 1-2, pp.

7-46.

A comprehensive early history of Hoare Logic appears in

Apt, K.R., Ten Years of Hoare Logic: A Survey”, ACM Transactions

on Programming Languages and Systems, October, 1981.

49 / 49

COMP1600 / COMP6260

slides created by: Dirk Pattinson

(with contributions by Victor Rivera and previous colleagues)

convenor: Pascal Bercher

lecturer: Michael Norrish

Australian National University

Semester 2, 2022

Recall: Hoare Logic

Basic Ingredient. Hoare-triples

{P} S {Q}

P and Q are predicates (formulae)

S is a code (fragment)

Example. {x > 0} while (x>0) do x := x-1 {x = 0}

Meaning. If we run S from a state that satisfies precondition P and if S

terminates, then the post-state will satisfy Q.

1 / 49

Hoare Logic

Idea. Proof Rules that allow us to prove all true triples.

Assignment

{Q(e)} x := e {Q(x)}

Precondition Strengthening / Postcondition Weakening

Ps → Pw {Pw} S {Q}

{Ps} S {Q}

{P} S {Qs} Qs → Qw

{P} S {Qw}

Sequence.

{P} S1 {Q} {Q} S2 {R}

{P} S1; S2 {R}

Conditional.

{P ∧ b} S1 {Q} {P ∧ ¬b} S2 {Q}

{P} if b then S1 else S2 {Q}

2 / 49

Proof Rule for While Loops (Rule 6/6)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b}

I is called the loop invariant.

I is true before we encounter the while statement, and remains true

each time around the loop (although not necessarily midway during

execution of the loop body).

If the loop terminates the control condition must be false, so ¬b

appears in the postcondition.

For the body of the loop S to execute, b needs to be true, so it

appears in the precondition.

3 / 49

Soundness of the While Rule w.r.t. the semantics

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b}

Soundness. If the premise is true, then so is the conclusion.

assume that I holds in the initial state.

if b is false, nothing happens, so I ∧ ¬b is true in post-state.

if b is true, then (by premise) I holds at end of each iteration

assuming that the loop terminates, b becomes false (and I still holds)

Q. What about non-termination?

4 / 49

Applying the While Rule

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

Difficult bit. Finding the right invariant.

This requires intuition and practice. There is no automated way of

doing this.

Easy bit. Establishing the desired postcondition

The postcondition we get after applying our rule has form I ∧ ¬b.

But if I ∧ ¬b → Q, we can use postcondition weakening.

Easy bit. Establishing the desired precondition

The precondition we get after applying our rule has form I . But if

P → I , we can use precondition strengtening.

5 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2. {I} while b do S {I ∧ ¬b} (While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6. {P} while b do S {Q} (Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2. {I} while b do S {I ∧ ¬b} (While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2.

{I} while b do S {I ∧ ¬b}

(While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1.

{I ∧ b} S {I}

2.

{I} while b do S {I ∧ ¬b}

(While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2.

{I} while b do S {I ∧ ¬b}

(While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2. {I} while b do S {I ∧ ¬b} (While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2. {I} while b do S {I ∧ ¬b} (While Loop, 1)

3.

I ∧ ¬b → Q

(Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2. {I} while b do S {I ∧ ¬b} (While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2. {I} while b do S {I ∧ ¬b} (While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2. {I} while b do S {I ∧ ¬b} (While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5.

P → I

(Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2. {I} while b do S {I ∧ ¬b} (While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6.

{P} while b do S {Q}

(Precondition Strengthening, 4, 6)

6 / 49

Applying the While Rule (schematic proof)

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b} {P} while b do S {Q}

1. {I ∧ b} S {I}

2. {I} while b do S {I ∧ ¬b} (While Loop, 1)

3. I ∧ ¬b → Q (Logic)

4. {I} while b do S {Q} (Postcondition Weakening, 2, 3)

5. P → I (Logic)

6. {P} while b do S {Q} (Precondition Strengthening, 4, 6)

6 / 49

Example

Goal. Find condition I to prove that:

{n > 3} while n>0 do n := n-1 {n = 0}

Observation. Need to prove the above using while-rule, i.e.

{I ∧ b} n := n− 1 {I}

{I} while (n>0) do n:= n-1 {I ∧ n ≤ 0}

Want. Loop invariant I such that

It is implied by the precondition:

n > 3→ I

if the loop terminates (i.e. n > 0 is false), then I should imply the

postcondition:

I ∧ n ≤ 0→ n = 0

If I is true and the body is executed, I is true afterwards:

{I ∧ n > 0} n := n− 1 {I}

Loop Invariant. I ≡ (n ≥ 0)

have {n ≥ 0 ∧ n > 0} n := n− 1 {n ≥ 0}

n ≥ 0 ∧ ¬(n > 0)→ n = 0

7 / 49

Example (cont.)

Goal. Find condition I to prove that:

{n > 3} while n>0 do n := n-1 {n = 0}

Loop Invariant. I ≡ (n ≥ 0), we have

n > 3→ n ≥ 0,

n ≥ 0 ∧ n ≤ 0→ n = 0, and

{n ≥ 0 ∧ n > 0} n := n− 1 {n ≥ 0}.

7 / 49

Example, Formally

1. {n − 1 ≥ 0} n := n− 1 {n ≥ 0} (Assignment)

2. n ≥ 0 ∧ n > 0→ n − 1 > 0 (Logic)

3. {n ≥ 0 ∧ n > 0} n := n− 1 {n ≥ 0} (Prec. Strength., 1, 2)

4. {n ≥ 0} while (n > 0) do n := n− 1 {n ≥ 0∧¬(n > 0)} (While Loop, 3)

5. n > 3→ n ≥ 0 (Logic)

6. {n > 3} while (n > 0) do n := n− 1 {n ≥ 0 ∧ ¬(n > 0)} (Prec.

Strength., 4, 5)

7. n = 0↔ n ≥ 0 ∧ ¬(n > 0) (Logic)

8. {n ≥ 0} while (n > 0) do n := n− 1 {n = 0} (Post. Equiv., 6, 7)

Other Invariants

e.g. true or n = 0

both are invariants, and give n = 0 as postcondition

but n ≥ 0 is better (weaker) as it is more general.

8 / 49

Let’s Prove a Program!

Program (with specification):

{True}

i:=0;

s:=0;

while (i ̸= n) do

i:=i+1;

s:=s+(2*i-1)

{s = n2}

(The sum of the first n odd numbers is n2)

Goal: prove

{True} Program {s = n2}

9 / 49

A Very Informal Analysis

Let’s look at some examples:

1 = 1 = 12

1 + 3 = 4 = 22

1 + 3 + 5 = 9 = 32

1 + 3 + 5 + 7 = 16 = 42 . . .

It looks OK - let’s see if we can prove it!

Goal: prove

{True} Program {s = n2}

10 / 49

How can we prove it?

First Task. Find a loop invariant I . (NB: S and s are different!)

Post condition and loop condition:

{I ∧ b} S {I}

{I} while b do S {I ∧ ¬b}

while (i ̸= n) do

i:=i+1; (1, 2, 3, ...)

s:=s+(2*i-1) (1, 4, 9, ...)

{s = n2}

Want. (I ∧ i = n)→ (s = n2) to apply postcondweak

Loop Body. Each time i increments, s moves to next square number.

Invariant. I ≡ s = i2.

11 / 49

Check I as (s = i2) is an invariant: prove {I}S{I}

{s = i2} i := i + 1 {Q} {Q} s := s + (2 ∗ i − 1) {s = i2}

Seq{s = i2} i := i + 1; s := s + (2 ∗ i − 1) {s = i2}

Using the assignment axiom and the sequence rule:

1. {Q} s:=s+(2*i-1) {s = i2}

2.

3. {s = i2} i:=i+1 {Q}

4. {s = i2} i:=i+1; s:=s+(2*i-1) {s = i2} (Sequence, 3, 1)

12 / 49

Check I as (s = i2) is an invariant: prove {I}S{I}

{s = i2} i := i + 1 {Q} {Q} s := s + (2 ∗ i − 1) {s = i2}

Seq{s = i2} i := i + 1; s := s + (2 ∗ i − 1) {s = i2}

Q is {s + (2 ∗ i − 1) = i2}

Using the assignment axiom and the sequence rule:

1. {s + (2 ∗ i − 1) = i2} s:=s+(2*i-1) {s = i2} (Assignment)

2.

3. {s = i2} i:=i+1 {s + (2 ∗ i − 1) = i2}

4. {s = i2} i:=i+1; s:=s+(2*i-1) {s = i2} (Sequence, 3, 1)

13 / 49

Check I as (s = i2) is an invariant: prove {I}S{I}

{s = i2} i := i + 1 {Q} {Q} s := s + (2 ∗ i − 1) {s = i2}

Seq{s = i2} i := i + 1; s := s + (2 ∗ i − 1) {s = i2}

Q is {s + (2 ∗ i − 1) = i2}

Using the assignment axiom and the sequence rule:

1. {s + (2 ∗ i − 1) = i2} s:=s+(2*i-1) {s = i2} (Assignment)

2. {s + (2 ∗ (i + 1)− 1) = (i + 1)2} i:=i+1 {s + (2 ∗ i − 1) = i2}

(Assignment)

3. {s = i2} i:=i+1 {s + (2 ∗ i − 1) = i2} (Prec. Equiv., 2)

4. {s = i2} i:=i+1; s:=s+(2*i-1) {s = i2} (Sequence, 3, 1)

So far, so good. (I as (s = i2) is an invariant.)

14 / 49

Completing the Proof of {True} Program {s = n2}

6 Strengthen the precondition to match the While rule premise

{I ∧ b} S {I}

{(s = i2) ∧ (i ̸= n)} i:=i+1; s:=s+(2*i-1) {s = i2}

7 Apply the While rule and postcondition equiv:

s = i2 ∧ i = n↔ s = n2

{s = i2} while ... s:=s+(2*i-1) {s = n2}

8 Check that the initialisation establishes the invariant:

{0 = 02} i:=0 {0 = i2} {0 = i2} s:=0 {s = i2}

{0 = 02} i:=0; s:=0 {s = i2}

9 (0 = 02) ↔ True, so putting it all together with Sequencing we have

{True} i := 0 ; s := 0 ; while (i ̸= n) do S {s = n2}

15 / 49

What about Termination?

Hoare Logic (in this form) proves partial correctness.

Example. while 1+1 = 2 do x:=0.

This will loop forever!

can still prove things about it

Exercise.

{True} while 1+1 = 2 do x:=0 {False}

Termination.

remember functional programs? Something must decrease

need loop variant (later)

16 / 49

Are the Rules Complete?

So far. Have a very simple language

new rules for arrays, for-loops, exceptions, . . .

Focus here. Soundness

every provable Hoare triple is (semantically) true

soundness holds but terms and conditions apply

with these assumptions, also have completeness, i.e. every true Hoare

triple is provable.

Completeness. if {P} S {Q} is true then {P} S {Q} is provable

17 / 49

What are these Assumptions?

The language we use for expressions in our programs is the same as

the language we use in our pre- and postconditions (in our case, basic

arithmetic).

We assumed no aliasing of variables. (In most real languages we can

have multiple names for the one piece of memory.)

How is aliasing a problem?

Suppose x and y refer to the same cell of memory.

▶ We get {y +1 = 5 ∧ y = 5} x:=y+1 {x = 5 ∧ y = 5} (Assignment)

▶ i.e. {y = 4 ∧ y = 5} x:=y+1 {x = 5 ∧ y = 5}

▶ i.e. if initial state satisfies False and x:=y+1 terminates then final state

satisfies {x = 5 ∧ y = 5} (but also works for x = 6 ∧ y = 6)

which makes a mockery of our calculus since it proves rubbish!

18 / 49

What are these Assumptions?

The language we use for expressions in our programs is the same as

the language we use in our pre- and postconditions (in our case, basic

arithmetic).

We assumed no aliasing of variables. (In most real languages we can

have multiple names for the one piece of memory.)

How is aliasing a problem?

Suppose x and y refer to the same cell of memory.

▶ We get {y +1 = 5 ∧ y = 5} x:=y+1 {x = 5 ∧ y = 5} (Assignment)

▶ i.e. {y = 4 ∧ y = 5} x:=y+1 {x = 5 ∧ y = 5}

▶ i.e. if initial state satisfies False and x:=y+1 terminates then final state

satisfies {x = 5 ∧ y = 5} (but also works for x = 6 ∧ y = 6)

which makes a mockery of our calculus since it proves rubbish!

18 / 49

Finding a Proof

Example.

{ n >= 0 }

f := 1;

i := n;

while (i > 0) do

f := f * i;

i := i-1;

{ f = n! }

19 / 49

Finding a Proof

Annotating the program: I = f ∗ i ! = n! ∧ i ≥ 0

{ n >= 0 }

f := 1;

{ f = 1 /\ n >= 0 } -- provable with assignment

i := n;

{ f = 1 /\ i = n /\ n >= 0} -- provable with assignment

==> -- use postcond weakening

{ I } -- general premise of while rule

while (i > 0) do

{ I /\ i > 0 } -- proof obligation for loop body

f := f * i; -- n, n * (n-1), n * (n-1) * (n-2) ...

i := i-1; -- n-1, n-2, n-3, ...

{ I } -- up until here.

{ I /\ not(i > 0) } -- general conclusion of while rule

==> -- use postcond weakening

{ f = n! }

Invariant: f * i! = n! / i >= 0

20 / 49

From Annotated Programs to Proofs

Initialisation Part

{ n >= 0 }

f := 1;

{ f = 1 /\ n >= 0 } -- provable with assignment

i := n;

{ f = 1 /\ i = n /\ n >= 0} -- provable with assignment

1. {f = 1∧ n = n∧ n ≥ 0} i := n {f = 1∧ i = n∧ n ≥ 0} (Assignment)

2. {1 = 1∧n = n∧n ≥ 0} f := 1 {f = 1∧n = n∧n ≥ 0} (Assignment)

3. n ≥ 0↔ 1 = 1 ∧ n = n ∧ n ≥ 0 (Logic)

4. {n ≥ 0} f := 1 {f = 1 ∧ n = n ∧ n ≥ 0} (Prec. Equiv. 2, 3)

5. {n ≥ 0} f := 1; i := n {f = 1 ∧ i = n ∧ n ≥ 0} (Sequence, 1, 4)

21 / 49

From Invariant to Loop Body

{ I } -- general premis of while rule

while (i > 0) do

{ I /\ i > 0 } -- proof obligation for loop body

f := f * i; -- n, n * (n-1), n * (n-1) * (n-2) ...

i := i-1; -- n-1, n-2, n-3, ...

{ I } -- up until here.

{ I /\ not(i > 0) } -- general conclusion of while rule

Invariant. I = f ∗ i ! = n! ∧ i ≥ 0

Loop Body: Proof obligation

{ f * i! = n! /\ i >= 0 /\ i > 0 }

f := f * i;

i := i - 1;

{ f * i! = n! /\ i >= 0}

22 / 49

From Annotated Programs to Proofs

Loop Body

{ f * i! = n! /\ i >= 0 /\ i > 0 } -- proof obligation

for loop body

f := f * i;

{ f * (i-1)! = n! /\ i >= 0 /\ i > 0} -- new annotation!

i := i-1;

{ f * i! = n! /\ i >= 0 } -- end loop body

6. {f ∗ (i − 1)! = n! ∧ (i − 1) ≥ 0} i := i− 1 {f ∗ i! = n! ∧ i ≥ 0}(Assignment)

7. {(f ∗ i) ∗ (i − 1)! = n! ∧ (i − 1) ≥ 0} f := f ∗ i {f ∗ (i − 1)! = n! ∧ (i − 1) ≥ 0} (Assignment)

8. f ∗ i! = n! ∧ i ≥ 0 ∧ i > 0→ (f ∗ i) ∗ (i − 1)! = n! ∧ (i − 1) ≥ 0 (Logic)

9. {f ∗ i! = n! ∧ i ≥ 0 ∧ i > 0} f := f ∗ i {f ∗ (i − 1)! = n! ∧ (i − 1) ≥ 0} (Prec. Stren., 7,8)

10. {f ∗ i! = n! ∧ i ≥ 0 ∧ i > 0} f := f ∗ i; i := i− 1 {f ∗ i! = n! ∧ i ≥ 0} (Sequence, 6,9)

23 / 49

From Annotated Programs to Proofs

Loop Body to While Loop

{ f * i! = n! /\ i >= 0 } -- premise of while

rule: "I"

while (i > 0) do

{ f * i! = n! /\ i >= 0 /\ i > 0 } -- "I /\ b"

f := f * i;

i := i-1;

{ f * i! = n! /\ i >= 0 } -- "I"

{ f * i! = n! /\ i >= 0 /\ not(i > 0) } -- conclusion of while:

"I /\ not b"

11. {f ∗ i ! = n! ∧ i ≥ 0}

while (i > 0) do { f:= f*i; i:= i-1}

{f ∗ i ! = n! ∧ i ≥ 0 ∧ ¬(i > 0)} (While, 10)

24 / 49

Putting it all together

{ n >= 0 }

f := 1;

i := n;

{ f = 1 /\ i = n /\ n >= 0} -- have already

==> -- postcond weakening

{ f * i! = n! /\ i >= 0 }

while (i > 0) do

f := f * i;

i := i-1;

{ f * i! = n! /\ i >= 0 /\ not(i > 0) } -- have already

==> -- postcond weakening

{ f = n! }

12. f = 1 ∧ i = n ∧ n ≥ 0→ f ∗ i ! = n! ∧ i ≥ 0 (Logic)

13. {n ≥ 0} f := 1; i := n {f ∗ i ! = n! ∧ i ≥ 0} (Postcond. Weak., 5, 12)

14. {n ≥ 0} program {f ∗ i ! = n! ∧ i ≥ 0 ∧ ¬(i > 0)} (Seq., 13, 11)

15. f ∗ i ! = n! ∧ i ≥ 0 ∧ ¬(i > 0)→ f = n! (Logic)

16. {n ≥ 0} program {f = n!} (Postcondition Weakening, 14, 15)

25 / 49

Hoare Logic: Total Correctness

Motto. Total Correctness = partial correctness + termination

New Notation.

[P] S [Q]

P and Q are precondition and postcondition, as before

S is a code fragment

Meaning. If the precondition holds, then executing S will terminate, and

the postcondition is true.

Example.

[P] S [true] – S always terminates from precondition P

{P} S {false} – S never terminates from precondition P

26 / 49

Rules for Total Correctness

Q. What are the rules for total correctness?

assignment

sequencing

conditional

pre/post strengthening/weakening

still work, as there’s no danger of non-termination.

Problematic Rule. while (may introduce non-termination)

27 / 49

Assignment, revisited

[Q(e)] x := e [Q(x)]

Assumptions. (fine for our toy language)

evaluation of expression e terminates.

evaluation of e returns a number (no exception e.g.)

In General.

the expression can be recursively defined

there may be errors, e.g. division by zero

28 / 49

Rules for Total Correctness

Ps → Pw [Pw ] S [Q]

[Ps ] S [Q]

(Precondition Strengthening)

[P] S [Qs ] Qs → Qw

[P] S [Qw ]

(Postcondition Weakening)

[P] S1 [Q] [Q] S2 [R]

[P] S1; S2 [R]

(Sequence)

[P ∧ b] S1 [Q] [P ∧ ¬b] S2 [Q]

[P] if b then S1 else S2 [Q]

(Conditional)

Assumption. Evaluation of b always terminates (OK here)

29 / 49

Termination of Loops

Example

[y > 0]

while (y < r) do

r := r - y;

q := q + 1

[true]

30 / 49

Termination of Loops

Example

[y > 0]

while (y < r) do

r := r - y;

q := q + 1

[true]

Observations.

q := q + 1 irrelevant

y doesn’t change, always positive

r strictly decreases in each iteration

y < r will eventually be false.

31 / 49

Termination of Loops: General Condition

Example

[y > 0]

while (y < r) do

r := r - y;

q := q + 1

[true]

Termination follows if we have a variant E that is,

E ≥ 0 at the beginning of each iteration

E strictly decreases at each iteration

Q. What could be a variant in this example?

32 / 49

While Rule for Total Correctness

Goal. Show that

[P] while b do S [Q]

In Addition to partial correctness (e.g. finding I ), find variant E such

that

E ≥ 0 at the beginning of each iteration:

I ∧ b → E ≥ 0

E is strictly decreasing in each iteration

[I ∧ b ∧ (E = n)] S [I ∧ E < n]

where n is an auxiliary variable not appearing elsewhere, to

“remember” initial value of E

33 / 49

While Rule for Total Correctness

I ∧ b → E ≥ 0 [I ∧ b ∧ E = n] S [I ∧ E < n]

[I ] while b do S [I ∧ ¬b]

where n is an auxiliary variable not appearing elsewhere.

Intuition.

E is an upper bound to the number of loop iterations

termination of functional programs: measure decrease in recursive call

34 / 49

Example

Goal. [y > 0] while (y < r) do r := r - y; q := q+1 [true]

Focus. Loop body r := r - y; q := q + 1

want some invariant: let’s just call it I

want some variant: here r is decreasing

First Goal. The variant is ≥ 0 when we enter the loop:

formally: I ∧ (y < r)→ r ≥ 0

this suggests I ≡ y > 0

Second Goal. The invariant is re-established, and the variant decreases

formally:

[(y > 0) ∧ (y < r) ∧ r = n] r := r = y; q:= q+1 [(y > 0) ∧ r < n]

this seems to be right, so let’s prove it!

35 / 49

Example Proof

Goal.

[(y > 0) ∧ (y < r) ∧ r = n] r := r - y; q:= q+1 [(y > 0) ∧ r < n]

First Assignment.

[(y > 0) ∧ (r < n)] q := q+ 1 [y > 0 ∧ r < n]

Second Assignment.

[(y > 0) ∧ (r − y < n)] r := r-y [y > 0 ∧ r < n]

Sequencing.

[(y > 0) ∧ (r − y < n)] r := r-y; q := q+1 [y > 0 ∧ r < n]

Precondition Strengthening.

[(y > 0) ∧ (y < r) ∧ (r = n)] r := r - y; q := q+1 [y > 0 ∧ r < n]

36 / 49

Completing the Proof

While Rule.

I ∧ b → E ≥ 0 [I ∧ b ∧ E = n] S [I ∧ E < n]

[I ] while b do S [I ∧ ¬b]

1. [(y > 0) ∧ (r < n)] q := q+ 1 [y > 0 ∧ r < n] (Assignment)

2. [(y > 0) ∧ (r − y < n)] r := r-y [y > 0 ∧ r < n] (Assignment)

3. [(y > 0) ∧ (r − y < n)] r := r-y; q := q+1 [y > 0 ∧ r < n] (Sequence, 2, 1)

4. (y > 0) ∧ (y < r) ∧ (r = n)→ (y > 0) ∧ (r − y < n) (Logic)

5. [(y > 0) ∧ (y < r) ∧ (r = n)] r := r-y; q := q+1 [y > 0 ∧ r < n] (Prec.

Streng., 2, 3)

6. (y > 0) ∧ (y < r)→ r ≥ 0 (Logic.)

7. [y > 0] while (y < r) do r:= r-y; q:= q+1 [y > 0 ∧ y ≥ r ] (While Loop, 5,

6)

8. y > 0 ∧ y ≥ r → true

9. [y > 0] while (y < r) do r:= r-y; q:= q+1 [true] (Postc. Weak., 7, 8)

37 / 49

Second Example

[n >= 0]

fact := 1;

i := n;

while (i > 0) do

fact := fact * i;

i := i - 1

[fact = n!]

Q1. What is the invariant (linking n, fact and i)?

before: fact = 1, i = n

1st iteration: fact = n, i = n-1

2nd iteration: fact = n * (n-1), i = n-2

...

last iteration: fact = n * ... * 1, i = 0

Invariant: fact ∗ i ! = n!

38 / 49

Second Example

[n >= 0]

fact := 1;

i := n;

while (i > 0) do

fact := fact * i;

i := i - 1

[fact = n!]

Q2. Is the invariant fact ∗ i ! = n! good enough?

true initially: for fact = 1 and i = n.

implies postcondition: fact ∗ i ! = n! ∧ ¬(i > 0)→ fact = n!

Stronger Invariant. fact ∗ i ! = n! ∧ i ≥ 0

39 / 49

Second Example

[n >= 0]

fact := 1;

i := n;

while (i > 0) do

fact := fact * i;

i := i - 1

[fact = n!]

Q3. What’s the variant?

i ≥ 0 for every iteration (I ∧ b → E ≥ 0)

decreases with every iteration

Variant. E ≡ i

40 / 49

Proof Skeleton

Simple Assignments.

[n >= 0]

fact := 1;

i := n;

[n >= 0 /\ fact = 1 /\ i = n]

Applying While

[ fact * i! = n! /\ i >= 0 ]

while (i > 0) do

fact := fact * i;

i := i - 1

[ fact * i! = n! /\ i >= 0 /\ i <= 0]

Missing Glue. Weakening / Strengthening

from postcondition of assignments to precondition of while

from postcondition of while to goal statement (fact = n!)

41 / 49

Zooming in on While

[ fact * i! = n! /\ i >= 0 ]

while (i > 0) do

fact := fact * i;

i := i - 1

[ fact * i! = n! /\ i >= 0 /\ i <= 0]

Loop Body (Invariant: fact ∗ i ! = n! ∧ i ≥ 0, Variant: i)

[fact * i! = n! /\ i >= 0 /\ i > 0 /\ i = a]

fact := fact * i;

i := i - 1

[ fact * i! = n! /\ i >= 0 /\ i < a]

Positivity Condition. fact ∗ i ! = n! ∧ i ≥ 0 ∧ i > 0→ i ≥ 0 (Maths)

42 / 49

While Rule: Soundness

I ∧ b → E ≥ 0 [I ∧ b ∧ E = n] S [I ∧ E < n]

[I ] while b do S [I ∧ ¬b]

Partial Correctness.

premises of the rule imply those of the rule for partial correctness

so if the loop terminates, the postcondition holds

Missing. Termination

43 / 49

Termination Analysis

I ∧ b → E ≥ 0 [I ∧ b ∧ E = n] S [I ∧ E < n]

[I ] while b do S [I ∧ ¬b]

Let σ be a state that validates the precondition I . If b is false in σ, we are

done. Assume that b is true in σ, hence the value of E in σ is ≥ 0.

Induction on the value σ(E ) of E in state σ.

Base case. σ(E ) = 0.

Right premise implies that E < 0 after one iteration

With left premise, get that ¬b after one iteration

hence the loop terminates after one iteration.

Step Case. Let σ(E ) = k + 1

after one iteration, have σ(E ) ≤ k

statement follows by induction hypothesis.

44 / 49

Variation: More Expressive Logic

So far. In triples {P} S {Q} we have

S a program fragment (we keep this for now)

P and Q propositional formulae made from basic arithmetic

Q. How about expressing the following?

{true} x := 2 ∗ x {even(x)}

A. We could say that even(x) = ∃y .2 ∗ y = x

Change. Allowing pre/postconditions to be first order formulae.

45 / 49

Example.

{true} x := 2 ∗ x {∃y .2 ∗ y = x}

Using the assignment axiom.

{∃y .2 ∗ y = 2 ∗ x} x := 2 ∗ x {∃y .2 ∗ y = x}

More Expressive Logic. Assertions are first-order formulae

all rules remain valid

Hoare-logic is (almost) insensitive to underlying logic

46 / 49

Variation: More Expressive Programs

Example Feature. Arrays

allow expressions to contain a[i ]

(we assume that the index is always in scope)

Maximum Finding

m := a[0]

i := 1;

while (i < n) do

if a[i] > m then m := a[i] else m := m;

i := i + 1

Q. How do we express that m is the maximum array element?

A. Use first order logic.

m is largest: ∀k .0 ≤ k < n→ m ≥ a[k]

m is in array: ∃k .0 ≤ k < n ∧m = a[k]

47 / 49

Annotated Code

{n >= 1}

m := a[0]

i := 1;

{m = a[0] /\ i = 1 /\ n >= 1 }

==>

{forall k. 0 <= k < i -> m >= a[k] /\ i <= n}

while (i < n) do

if a[i] > m then m := a[i] else m := m;

i := i + 1

{forall k. 0 <= k < i -> m >= a[k] /\ i <= n /\ i >= n}

==>

{forall k. 0 <= k < n -> m <= a[k]}

Invariant. I ≡ ∀k .0 ≤ k < i → m ≤ a[k] ∧ i ≤ n

initially: m = a[0] ∧ i = 1→ I

at end: I ∧ i ≥ n→ ∀k .0 ≤ k < n→ m ≤ a[i ]

Remark. Can turn this into a formal proof as before.

48 / 49

References

The textbook has material on Hoare Logic

Grassman & Tremblay, “Logic and Discrete Mathematics: A

Computer Science Perspective”, Prentice-Hall, Chapter 9, pp.

481-518.

Some nice online notes with lots of examples:

Gordon, “Specification and Verification I”, http://www.cl.cam.ac.

uk/~mjcg/Lectures/SpecVer1/SpecVer1.html, Chapters 1-2, pp.

7-46.

A comprehensive early history of Hoare Logic appears in

Apt, K.R., Ten Years of Hoare Logic: A Survey”, ACM Transactions

on Programming Languages and Systems, October, 1981.

49 / 49