The Australian National University Semester 2, 2020 Research School of Computer Science Tutorial 6 and
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. Solution.
1. for x = 0 to hold in the postcondition, we need that x is decremented to zero, i.e. we require a = 0. If x is negative initially, then the loop will not be executed, and x will be negative in the post-state, so the postcondition will also be false. We therefore require P = (a = 0) ∧ (x ≥ 0).
2. Wegiveaproofof{(a=0)∧(x≥0)}while x>a do x:=x-1{x=0}inlinearform. For the invariant I we require that
• {I∧x>a}x:=x−1{I},i.e.wecanprovethepremiseofthewhilerule
• a = 0 ∧ x ≥ 0 → I, i.e. the overall precondition implies the conclusion of the while-rule.
• I ∧ ¬(x > a) → x = 0, i.e. postcondition of the while rule implies the overall intended postcondition.
As invariant, we therefore chose I = (a = 0) ∧ (x ≥ a). This gives the following proof:
1. {a=0∧x−1≥a}x:=x−1{(a=0)∧(x≥a)}(Assignment)
2. (a=0)∧(x≥a)∧(x>a)→a=0∧(x−1≥a)(BasicMaths)
3. {a=0∧x≥a∧x>a}x:=x−1{a=0∧x≥a}(PreconditionStrengthening,2,1)
4. {a=0∧x≥a}while x>a do x:= x-1{a=0∧x≥a∧¬(x>a)}(WhileLoop,3) 5. a=0∧x≥a∧¬(x>a)→x=0(BasicMaths)
6. {a = 0 ∧ x ≥ a} while x>a do x:= x-1 {x = 0} (Postcondition Weakening, 4, 5)
Exercise 2
Consider the following Hoare triple:
{ i = 0 /\ s = 0 /\ n >= 0 }
while (i < n) do
i := i + 1;
s := s + i
{ s = n * (n+1) / 2 }
Find the Invariant
1
1. Complete the table below
loop iteration 0 1 2 3 4 i0
s0
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. Solution. We complete the table as follows:
loopiteration 0 1 2 3 4 i01234
s 0 1 1+2 1+2+3 1+2+3+4
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.
Solution. With a view to the postcondition, we note that I ≡ s = 1+2+. . .+i. Using the fact that ik=1 k = i∗(i+ 1)/2, we can write the invariant as I ≡ s = i∗(i+1)/2. Another possible invariant is I ≡ s = i∗(i+1)/2∧i ≤ n.
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. Solution. For the invariant I ≡ s = i ∗ (i + 1)/2 we would need to prove that
s = i ∗ (i + 1)/2 ∧ ¬(i < n) → s = n ∗ (n + 1)/2
which is not true (e.g. for i = 0 and s = 0 and n = 12 we have both s = i ∗ (i + 1)/2 (as 0 = 0 ∗ (0 + 1)/2) and
¬(i < n) (as it is false that 0 < 12), but we clearly do not have that s = n ∗ (n + 1)/2, as 0 ̸= 12 ∗ 13/2.
The missing piece of information is that at the end of the loop, the variable i will be exactly equal to n, whereas the negation of the loop condition (¬(i < n)) just gives us that i ≥ n. However, in every iteration of the loop, we know thati≤nwhichiswhatweaddtoourinvariant.ThemodifiedinvariantthusisI ≡s=i∗(i+1)/2∧i≤n.
For this modified invariant, we obtain that I ∧¬(i ≤ n) → s = n∗(n+1)/2, because assuming P ∧¬(i ≤ n) we have that
• s=i∗(i+1)/2∧i≤n(bywritingoutI)
• i≥n(byexpandingout¬(i≤n))
• thereforei=n,asbothi≤nandi≥n
• andhences=n∗(n+1)/2giventhats=i∗(i−1)/2andi=n.
4. Hence, or otherwise, give a Hoare Logic proof of the Hoare triple above. Solution. The complete proof is as follows:
1. 2. 3. 4. 5. 6. 7. 8. 9.
10.
Exercise 3
{s+i=i(i+1)/2∧i≤n}s := s + i{s=i(i+1)/2∧i≤n}(Assignment)
{s+(i+1) = (i+1)(i+1+1)/2∧i+1 ≤ n} i := i + 1 {s+i = i(i+1)/2∧i ≤ n} (Assignment) s=i(i+1)/2∧i≤n∧i
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:
• itshouldbe≥0whentheloopisentered,i.e.I∧(i
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:
• itshouldbestrongenoughtoimplythepostconditioniftheloopconditionisfalse: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.
Solution.
1. Beforewerunthecode,wehavethatn ≥ 1,andafterwerunthecode,wecanguaranteethatn ≥ 1,p = 0and i=1.Hence,wechoosethemidconditionM =n≥1∧p=0∧i=1andgivethefollowingproof.
1. {n≥1∧p=0∧1=1}i:=1{n≥1∧p=0∧i=1}(Assignment)
2. {n≥1∧0=0∧1=1}p:=0{n≥1∧p=0∧1=1}(Assignment)
3. {n≥1∧0=0∧1=1}p:=0;i:=1{n≥1∧p=0∧i=1}(Sequence,1,2) 4. (n≥1)→(n≥1∧0=0∧1=1)(BasicMaths)
5. {n≥1}p:=0;i:=1{n≥1∧p=0∧i=1}(PreconditionStrengthening,3,4) 4
2. We draw a table showing the state of the variables, as shown:
loop iteration 0 1 2 3 4 p 0 m 2m 3m 4m i12345
From this table, we guess the invariant I ≡ p = m ∗ (i − 1). Unfortunately, it is still too weak, as I ∧ ¬b ≡ p = m ∗ (i − 1) ∧ i > n ̸→ p = m ∗ n.
Given I ∧ ¬b, we have that p = m ∗ (i − 1) and that i > n ≡ i ≥ n + 1. The minimum extra information required to conclude that p = m ∗ n would be if we also had that i ≤ n + 1 (which is an invariant property, as the code stops runningwheni≤nisfalse.)Hence,wechooseasourinvariantI ≡p=m∗(i−1)∧i≤n+1,andgivethe following proof:
6. {p=m∗(i+1−1)∧(i+1)≤n+1}i:=i+1{p=m∗(i−1)∧i≤n+1}(Assignment)
7. {p+m = m∗(i+1−1)∧(i+1) ≤ n+1} p := p + m {p = m∗(i−1+1)∧i+1 ≤ n+1} (Assignment)
8. {p+m = m∗(i+1−1)∧i+1 ≤ n+1} p := p + m;i := i + 1 {p = m∗(i−1)∧i ≤ n+1} (Sequence, 6, 7)
9. p=m∗(i−1)∧i≤n+1∧i≤n→p+m=m∗(i+1−1)∧i+1≤n+1(BasicMaths)
10. {p=m∗(i−1)∧i≤n+1∧i≤n}body{p=m∗(i−1)∧i≤n+1}(PreconditionStrengthening,8,
9)
3. Weapplythewhile-ruleandgluethepiecestogetherwithpreconditionstrengtheningandpostconditionweakening.
We write program for the entire program (in the last line of the proof)
11. {I} while (i <= n) do body {I ∧ ¬(i ≤ n)} (While Loop, 10)
12. M → I (Basic Maths, M the mid-condition above)
13. {M } while (i <= n) do body {I ∧ ¬(i ≤ n)} (Precondition Strengthening, 11, 12) 14. I∧¬(i≤n)→p=m∗n(BasicMaths,notethati≤n+1∧¬(i≤n)→i=n+1) 15. {M } while (i <= n) do body {p = m ∗ n} (Postcondition Weakening, 13, 14)
16. {n ≥ 1} program {p = m ∗ n} (Sequence, 5, 15)
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:
• itshouldbe≥0whentheloopisentered,i.e.I∧b→E≥0
• itshoulddecreaseeverytimetheloopbodyisexecuted,i.e.[I∧b∧E=k]body[I∧E
while (z
while (z