The aim of this assignment is to consolidate your understanding of the course's material on weakest precondition reasoning. It is worth 15% of your final mark for the course.

Instructions: Upload a pdf document with your solution to Gradescope by the due date and time. You may use the Word template A1-template.docx as your starting point, or copy the format of the template in A1-template.pdf to use with an editor other than      Word. For Question 2, add your wp reasoning in the spaces between the lines of code.

1. Prove the following justifying each line of your proof with a law from Appendix A of Programmingfrom Specifications.

a)    A ==> A && B      =      A ==> B     (1 mark)

b)    (A ==> B) && (!A ==> B)        =   B   (4 marks)

You do not need to state the laws for commutativity of && and || (A.2 and A.3) if you use them, but all other laws used must be stated.

2. The method DivMod below calculates the quotient and modulus of its inputs a and b using only addition, subtraction and multiplication and division by 2. Use weakest precondition      reasoning to show that it is partially correct.      (10 marks)

function Power(k: nat): nat {

if k == 0 then 1 else 2*Power(k - 1)

}

method DivMod(a: int, b: int) returns (q: int, r: int)

requires a >= 0 && b > 0

ensures a == q*b + r && 0 <= r < b

{

var c := b;

var k := 0;

while c <= a

invariant k >= 0 && c == Power(k)*b && a >= 0

{

c, k := 2*c, k + 1;

}

q, r := 0, a;

while c != b

invariant k >= 0 && c == Power(k)*b && a == q*c + r && 0 <= r < c

{

q, c, k := q*2, c/2, k - 1;

if r >= c {

q, r := q + 1, r - c;

}

}

}

Hints: Be careful with integer division: dividing 2*c by 2 is c, but multiplying c/2 by 2 is only equal to c when c is even.

The laws proved in Question 1 will be helpful in simplifying your predicates. If you use them refer to them as (1a) and (1b). Also, don't forget you can strengthen your predicates whenever that will help. For example, if you can't apply the laws from Question 1 where you think they would be useful, try strengthening your predicate.