The Australian National University School of Computing
Dirk Pattinson and
Semester 2, 2021 Practical Session 5
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 5
At the end of this tutorial, you will be able to prove the partial correctness (loop-less) of imperative programs using Hoare Logic.
Exercise 1 Hoare Logic: Semantics
Determine the truth value of the following Hoare triples and give your reasoning. You are not required to use Hoare Logic to prove these!
1. {j=a}j:=j+1{a=j+1}
False. Consider the case of a = j = 0; the precondition is satisfied, but after the assignment a = 0 and j = 1 and
the postcondition is false.
2. {i > j} j:=i+1; i:=j+1 {i > j}
Solution. True. Regardless of the initial state, the computation ends by making i = j + 1 and so i > j is satisfied.
3. {i ̸= j} if i>j then m:=i-j else m:=j-i {m > 0}
Solution. True. If i > j then m will be assigned a positive quantity. The other possibility is that i < j, given that the precondition holds, and again m will be assigned a positive number.
Exercise 2 Assignment Axiom
Prove each of the following. The first one has been done for you in detail, but you can just give the line numbered steps and their justifications.
1. {i=5}a:=i+2{(a=7)∧(i=5)}
We apply the ‘copy-and-replace’ assignment axiom. The precondition this generates doesn’t look exactly like the one we are asked for, but it is equivalent to it:
1. {(i + 2 = 7) ∧ (i = 5)} a := i + 2 {(a = 7) ∧ (i = 5)} 2. (i + 2 = 7) ∧ (i = 5) ↔ i = 5
3. {i = 5} a := i + 2 {(a = 7) ∧ (i = 5)}
(Assignment) (Logic) (Precondition Equivalence, 1, 2)
We could have used precondition strengthening instead of precondition equivalence here. 2. {(i=5)∧(a=3)}a:=i+2{a=7}
Solution. Again we start with the assignment axiom, but this time the precondition we generate is not equivalent to the one we want - it is too weak. Hence we must invoke precondition strengthening:
1. {i + 2 = 7} a := i + 2 {a = 7} 2.(i=5 ∧ a=3) → (i+2=7)
3. {(i = 5) ∧ (a = 3)} a := i + 2 {a = 7}
3. {i=a−1}i:=i+2{i=a+1}
Solution. Assignment axiom, then precondition equivalence, once again.
Exercise 3 Control Structures
(Assignment) (BasicMaths.&Logic) (Precondition Strengthening, 1, 2)
Prove each of the following. The first one has been done for you. You need only give the formal proof steps and their
justifications.
1. {a>b}m:=1; n:=a-b{m∗n>0}
Start at the end of the program, and apply the assignment axiom to the command n := a − b and the given post- condition. This generates the precondition m ∗ (a − b) > 0. Apply the assignment axiom again with this new intermediate assertion and m := 1, rearrange the precondition we generate from this to get a > b, then use the sequencing rule to stick the proof together.
Exercise 4
More on Semantics
1. {m ∗ (a − b) > 0} n := a − b {m ∗ n > 0} 2. {1 ∗ (a − b) > 0} m := 1 {m ∗ (a − b) > 0} 3. 1 ∗ (a − b) > 0 ↔ a > b
4. {a > b} m := 1 {m ∗ (a − b) > 0}
(Assignment) (Assignment) (Logic) (Precondition Equivalence, 2, 3) (Sequence, 4, 1)
(Assignment) (Assignment) (Logic) (Precondition Equivalence, 2, 3) (Sequence, 1, 4)
5. {a > b} m := 1; n := a − b {m ∗ n > 0}
2. {s = 2i} i:=i+1; s:=s*2 {s = 2i}
1. {s ∗ 2 = 2i} s := s ∗ 2 {s = 2i}
2. {s ∗ 2 = 2i+1} i := i + 1 {s ∗ 2 = 2i} 3.s∗2=2i+1 ↔s=2i
4. {s = 2i} i := i + 1 {s ∗ 2 = 2i}
5. {s = 2i} i := i + 1; s := s ∗ 2 {s = 2i}
LHS of Step 3 is valid because we can divide both sides of the equation by 2. Note also that we have proved that (s = 2i) is an invariant for this code.
3. {T rue} if i
Solution. False. Consider the case that i is negative. For example, if i = j = −1 initially, then the postcondition
will be false.
2. {i=3∗j}if i>j then m:=i-j else m:=j-i {m−2∗j =0}
Solution. False. If i = −3 and j = −1 then m will end up as 2, and so the postcondition will not hold.
3. {a=0}while x>a do x:=x-1{x=0}
Solution. False. If initially x = −1, or any other negative number, then the loop terminates with no iterations and x is unchanged.
Exercise 5
Prove each of the following.
More on Assignment Axiom
1. {i=5}a:=i+2{(a=7)∧(i>0)}
Solution. This follows by the same reasoning as Exercise 2.1 above – the assignment axiom, then precondition
equivalence. Alternatively, we could apply postcondition weakening to the result of Exercise 2.1.
2. {a=7}i:=i+2{a=7}
Solution. This question is a trivial assignment axiom one-liner. The importance of the example is that you often want to know that some variable’s value is not affected by the execution of some given code. This is a sort of invariant.
3. {True}a:=i+2{a=i+2}
1. {a = 7} i := i + 2 {a = 7} (Assignment)
Solution. Assignment axiom and precondition equivalence again. The only thing that is a little unusual is the constant True as the precondition, so discuss what this means (that if the code fragment terminates then it does so fulfilling the postcondition, whatever the opening state might have been). What might it mean if False was the precondition?
Exercise 6
1. {i + 2 = i + 2} a := i + 2 {a = i + 2} 2. T rue ↔ i + 2 = i + 2
3. {T rue} a := i + 2 {a = i + 2}
Control Structures (2)
(Assignment) (Logic) (Precondition Equivalence, 1, 2)
1. Prove the following Hoare triple: {(i > 0) ∧ (j > 0)} if i
1. {i > 0} min := i {min > 0}
2.i>0∧j >0∧i
3.{i>0∧j >0∧i
4. {j > 0} min := j {min > 0}
5.i>0∧j >0∧¬(i
6.{i>0∧j >0∧¬(i
7.{i>0∧j >0}ifi
2. Consider the following Hoare triple:
{x=y}if (x=0) then x:=y+1 else z:=y+1{(z=1)→(x=1)} • determine whether it is valid or not
• if it is not valid, justify why this is the case by giving values for the variables that satisfy the precondition, and argue that the postcondition is not true after running the code
• if it is valid, give a proof in Hoare logic. Solution.
(a) This Hoare triple is valid. We give the following Hoare logic proof:
1 {z=1→y+1=1}x := y+1{z=1→x=1}(Assignment)
2 (x=y∧x=0)→(z=1→y+1=1)(BasicLogic)
3 {x=y∧x=0}x := y+1{z=1→x=1}(PreconditionStrengthening,1,2)
4 {y+1=1→x=1}z := y+1{z=1→x=1}(Assignment)
5 (x=y∧x̸=0)→(y+1=1→x=1)(BasicLogic)
6 {x=y∧x̸=0}z := y+1{z=1→x=1}(PreconditionStrengthening,4,5)
7 {x = y} if (x=0) then x:=y+1 else z:=y+1 {(z = 1) → (x = 1)} (Conditional, 3, 6)
(BasicLogic) (PreconditionStrengthening,1,2) (Assignment) (BasicLogic) (PreconditionStrengthening,4,5)
(Assignment)
Appendix — Hoare Logic Rules
• Assignment:
• Precondition Strengthening:
{Q(e)} x := e {Q(x)} Ps →Pw {Pw}S{Q}
{Ps} S {Q} You can always replace predicates by equivalent predicates,
i.e. if Ps ↔ Pw; just label your proof step with ‘precondition equivalence’. • Postcondition Weakening:
{P}S{Qs} Qs →Qw {P} S {Qw}
You can always replace predicates by equivalent predicates,
i.e. if Qs ↔ Qw; just label your proof step with ‘postcondition equivalence’.
• Sequence:
• Conditional:
{P} S1 {Q} {Q} S2 {R} {P}S1;S2 {R}
{P ∧b}S1 {Q} {P ∧¬b}S2 {Q} {P } if b then S1 else S2 {Q}