The Australian National University Semester 2, 2018 Research School of Computer Science Tutorial 7 Dirk Pattinson 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. Exercise 1 Hoare Logic: Simple Loops Consider the Hoare triple fPgwhile x>a do x:=x-1fx = 0g 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 (in linear form) 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. We give a proof of f(a = 0) ^ (x 0)g while x>a do x:=x-1 fx = 0g in linear form. For the invariant I we require that fI ^ x > ag x := x 1 fIg, i.e. we can prove the premise of the while rule 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. fa = 0 ^ x 1 ag x := x 1 f(a = 0) ^ (x a)g (ass) 2. (a = 0) ^ (x a) ^ (x > a) ! a = 0 ^ (x 1 a) (maths) 3. fa = 0 ^ x a ^ x > ag x := x 1 fa = 0 ^ x ag (precond strength, 2, 1) 4. fa = 0 ^ x ag while x>a do x:= x-1 fa = 0 ^ x a ^ :(x > a)g (while, 3) 5. a = 0 ^ x a ^ :(x > a) ! x = 0 (maths) 6. fa = 0 ^ x ag while x>a do x:= x-1 fx = 0g (postond weak, 4, 5) Exercise 2 More While Loops Give a proof of the following Hoare-triples, where you may use that we have established the validity of fs = 2ig i:=i+1; s:=s*2 fs = 2ig in Tutorial 6. 1. fs = 2ig while i= 1} while (z= 1} while (z= 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 P 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: P ^:(i n) ! p = mn it should be weak enough so that it is implied by the mid-condition M, that is M ! P. it should be an invariant, i.e fP ^ (i n)g body fPg should be provable. State the invariant, and give a Hoare-Logic proof of fP ^ (i < n)g body fPg 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. We postulate the midcondition M = n 1 ^ p = 0 ^ i = 1 and give the following proof. 1. fn 1 ^ p = 0 ^ 1 = 1g i := 1 fn 1 ^ p = 0 ^ i = 1g (ass) 2. fn 1 ^ 0 = 0 ^ 1 = 1g p := 0 fn 1 ^ p = 0 ^ 1 = 1g (ass) 3. fn 1 ^ 0 = 0 ^ 1 = 1g p := 0; i := 1 fn 1 ^ p = 0 ^ i = 1g (seq, 1, 2) 4. (n 1) ! (n 1 ^ 0 = 0 ^ 1 = 1) (maths) 5. fn 1g p := 0; i := 1 fn 1 ^ p = 0 ^ i = 1g (precond str, 3, 4) 2. We postulate the invariant P p = m (i 1) ^ i n + 1 and give the following proof: 6. fp = m (i + 1 1) ^ (i + 1) n + 1g i := i + 1 fp = m (i 1) ^ i n + 1g (ass) 7. fp + m = m (i + 1 1) ^ (i + 1) n + 1g p := p + m fp = m (i 1 + 1) ^ i + 1 n + 1g (ass) 8. fp + m = m (i + 1 1) ^ i + 1 n + 1g p := p + m; i := i + 1 fp = m (i 1) ^ i n + 1g (seq, 6, 7) 9. p = m (i 1) ^ i n + 1 ^ i n ! p + m = m (i + 1 1) ^ i + 1 n + 1 (maths) 10. fp = m (i 1) ^ i n + 1 ^ i ng body fp = m (i 1) ^ i n + 1g (precond str, 8, 9) 3. We apply the while-rule and glue the pieces together with precondition strengthening and postcondition weakening. We write program for the entire program (in the last line of the proof) 11. fPg while (i <= n) do body fP ^ :(i n)g (while, 10) 12. M ! P (maths, M the mid-condition above) 13. fMg while (i <= n) do body fP ^ :(i n)g (precon strength, 11, 12) 14. P ^ :(i n) ! p = m n (maths, note that i n + 1 ^ :(i n) ! i = n + 1) 15. fMg while (i <= n) do body fp = m ng (postcond weak, 13, 14) 16. fn 1g program fp = m ng (seq, 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 P as in the previous exercise, the variant should have the following two properties: it should be 0 when the loop is entered, i.e. P ^ b ! E 0 it should decrease every time the loop body is executed, i.e. [P ^ b ^ E = k] body [P ^ 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). Solution. We chose the variant E n i. 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 [P ^ b ^ E = k] body [P ^ E < k], and argue that P ^ b ! E 0. Solution. Recall that the invariant is P p = m (i 1) ^ i n + 1 and the loop condition is b i n. This means that P ^ b is equivalent to p = m (i 1) ^ i n + 1 ^ i n. In particular, this implies i n, hence n i 0. We give the following Hoare-Logic proof: 1. [p = m (i + 1 1) ^ i + 1 n + 1 ^ n (i + 1) < k]i := i + 1[p = m (i 1) ^ i n + 1 ^ n i < k] (ass) 2. [p + m = m (i + 1 1) ^ i + 1 n + 1 ^ n (i + 1) < k]p := p + m[p = m (i + 1 1) ^ i + 1 n + 1 ^ n (i + 1) < k] (ass) 3. [p + m = m (i + 1 1) ^ i + 1 n + 1 ^ n (i + 1) < k]p := p + m; i := i + 1[p = m (i 1) ^ i n + 1 ^ n i < k] (seq, 1, 2) 4. p = m (i 1) ^i n+ 1 ^i n^ni = k ! p+m = m (i+ 1 1) ^i+ 1 n+ 1 ^n (i+ 1) < k (maths) 5. [p = m(i1)^i n+1^i n^ni = k]p := p + m; i := i + 1[p = m(i1)^i n+1^ni < k] (precond strength, 3, 4) 3. Hence, or otherwise, give a Hoare-logic proof of [P] while (i <= n) do body [P ^ :b]. Solution. We continue the above proof. 6. P ^ b ! E 0 (maths, argued above) 7. [P] while (i<= n) do body [P ^ :b] (while, 5, 6). Appendix Hoare Logic Rules Assignment: fQ(e)g x := e fQ(x)g Precondition Strengthening: Ps ! Pw fPwg S fQg fPsg S fQg Postcondition Weakening: fPg S fQsg Qs ! Qw fPg S fQwg Sequence: fPg S1 fQg fQg S2 fRg fPg S1; S2 fRg Conditional: fP ^ bg S1 fQg fP ^ :bg S2 fQg fPg if b then S1 else S2 fQg While Loop: fP ^ bg S fPg fPg while b do S fP ^ :bg While Loop (Total Correctness): P ^ b ! E 0 [P ^ b ^ E = n] S [P ^ E < n] [P] while b do S [P ^ :b] where n is an auxilliary variable not appearing anywhere else.