The Australian National University School of Computing
Dirk Pattinson and
Semester 2, 2021 Practical Session 6
Foundations of Computation
The practical contains a number of exercises designed for the students to practice the course content. During the practical session, the tutor will work through some of these exercises while 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 the practical session.
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. Complete the table below
loop iteration 0 1 2 3 4 i0
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 = 1 and s = 1 and n = 0 we have both s = i ∗ (i + 1)/2 (as 1 = 1 ∗ (1 + 1)/2) and
¬(i < n) (as it is false that 1 < 0), but we clearly do not have that s = n ∗ (n + 1)/2, as 1 ̸= 0 ∗ 1/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 I ∧ ¬(i < n) we have that
• s=i∗(i+1)/2∧i≤n(bywritingoutI)
• i≥n(byexpandingout¬(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
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,
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.
while (i <= n) do
[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