The Australian National University Semester 2, 2020
Research School of Computer Science Tutorial 6
Dirk Pattinson and Victor Rivera
Foundations of Computation
The tutorial contains a number of exercises designed for the students to practice the course content. During the lab,
the tutor will work through some of these exercises while the students will be responsible for completing the remaining
exercises in their own time. There is no expectation that all the exercises will be covered in lab time.
Covers: Lecture Material Week 6
At the end of this tutorial, you will be able to prove the partial and total correctness of imperative programs using Hoare
Logic.
Exercise 1 Hoare Logic: Simple Loops
Consider the Hoare triple
{P}while x>a do x:=x-1{x = 0}
where P is an (as of yet unspecified) predicate.
1. find the weakest precondition P (in terms of x and a) that makes this Hoare-triple true. Justify your answer briefly
(no formal proof required).
2. Give a proof of validity of this triple, using the precondition P that you have identified above.
Exercise 2 Find the Invariant
Consider the following Hoare triple, where n ≥ 0 is an unspecified integer:
{ i = 0 /\ s = 0 }
while (i < n) do
i := i + 1
s := s + i;
{ s = n * (n+1) / 2 }
1. Complete the table below
loop iteration 0 1 2 3 4
i 0
s 0
by filling in the values of i and s after the first, second, etc. iteration of the loop. The values for the 0th loop iteration
are the initial values of i and s that are given by the precondition.
2. Using the table above, derive an invariant I, that is, a relation between s and i, that holds both before the loop is
being entered, and after each iteration of the loop body.
3. Check whether the invariant that you have found is strong enough so that – together with the negation of the loop
condition – implies the desired postcondition, and if not, modify the invariant accordingly.
That is, verify whether I ∧ ¬(i < n) → s = n ∗ (n + 1)/2, and modify the invariant if this is not the case.
4. Hence, or otherwise, give a Hoare Logic proof of the Hoare triple above.
Exercise 3 Find The Variant
Consider the following Hoare triple, but now formulated in terms of total correctness, where again n ≥ 0 is an unspecified
integer.
1
[ i = 0 /\ s = 0 ]
while (i < n) do
i := i + 1
s := s + i;
[ s = n * (n+1) / 2 ]
1. Identify and state a variant E for the loop. Using the same invariant I as in the previous exercise, the variant should
have the following two properties:
• it should be ≥ 0 when the loop is entered, i.e. I ∧ (i < n) → E ≥ 0
• it should decrease every time the loop body is executed, i.e. [I ∧ b ∧ E = k] body [I ∧ E < k]
where body stands for the body of the loop. You just need to state the variant, and do not need to prove the two
bullet points above (yet).
2. For the variant E that you have identified, give a proof of the premise of the while-rule for total correctness, i.e.
give a Hoare-logic proof of [I ∧ (i < n) ∧ E = k] body [I ∧ E < k], and argue that I ∧ (i < n) → E ≥ 0.
3. Hence, or otherwise, give a Hoare-logic proof of [I] while (i <= n) do body [I ∧ ¬b].
Exercise 4 More While Loops
Give a proof of the following Hoare-triples, where you may use that we have established the validity of {s = 2i}
i:=i+1; s:=s*2 {s = 2i} in Tutorial 5.
1. {s = 2i} while i2. {(s = 2i
) ∧ (i ≤ n)} while iExercise 5 Multiplication (Partial Correctness)
Consider the following (annotated) program that multiplies two numbers by means of repeated addition:
{n >= 1}
p := 0;
i := 1;
while (i <= n) do
p := p+m;
i := i+1
{p = m * n}
1. Identify the strongest mid-condition M for which the Hoare-triple
{n >= 1}
p := 0;
i := 1;
{ M }
is provable, and give a Hoare-logic proof of this fact.
2. Identify an invariant I for the loop. The invariant should have the following three properties:
• it should be strong enough to imply the postcondition if the loop condition is false: I ∧¬(i ≤ n) → p = m∗n
• it should be weak enough so that it is implied by the mid-condition M, that is M → I.
• it should be an invariant, i.e {I ∧ (i ≤ n)} body {I} should be provable.
State the invariant, and give a Hoare-Logic proof of {I ∧ (i < n)} body {I} where body is the body of the
while-loop.
3. Using the above, give a proof of the Hoare-triple given by the annotated program at the beginning of the exercise.
2
Exercise 6 Multiplication (Total Correctness)
We consider the same program fragment as above, but now the goal is to establish total correctness.
[n >= 1]
p := 0;
i := 1;
while (i <= n) do
p := p+m;
i := i+1
[p = m * n]
1. Identify and state a variant E for the loop. Using the same invariant I as in the previous exercise, the variant should
have the following two properties:
• it should be ≥ 0 when the loop is entered, i.e. I ∧ b → E ≥ 0
• it should decrease every time the loop body is executed, i.e. [I ∧ b ∧ E = k] body [I ∧ E < k]
where body stands for the body of the loop. You just need to state the variant, and do not need to prove the two
bullet points above (yet).
2. For the variant E that you have identified, give a proof of the premise of the while-rule for total correctness, i.e.
give a Hoare-logic proof of [I ∧ b ∧ E = k] body [I ∧ E < k], and argue that I ∧ b → E ≥ 0.
3. Hence, or otherwise, give a Hoare-logic proof of [I] while (i <= n) do body [I ∧ ¬b].
Exercise 7 Fibonacci Numbers
Recall the Fibonacci numbers defined by f(0) = 0, f(1) = 1 and f(n) = f(n − 2) + f(n − 1) for n ≥ 2 and consider
the following code fragment that we have annotated with pre and postcondition.
{ x = 0 /\ y = 1 /\ z = 1 /\ n >= 1}
while (z