Here's problem 6.h (corrected). h. (Cohen's exercise 9.7) Develop a different solution for S0 (the choice of a d to satisfy 1 <= d /\ d * y <= r on page 145). Arrive at a different invariant by deleting the conjunct R1 from RR. Division of a power of 2 by a power of 2 is allowed (i.e., shifting right), but exponentiation is not. Let's state the problem more clearly first. The annotated proof outline from Cohen's section 9.4 is as follows. {x >= 0 /\ y > 0} q,r := 0,x {invariant P: 0 <= r /\ q*y + r = x} ;do r >= y -> {P /\ r >= y} |[ var d, dd: int {P} ;S0 {P /\ (R0: 1 <= d) /\ (R1: d*y <= r) /\ (R2: dd = d * y) /\ (R3: d is a power of 2) /\ (R4: r < 2 * d * y)} ;r,q := r-dd, q+d {P} |] {P} od {P /\ ~(r >= y), hence R: 0 <= r /\ q*y + r = x /\ r < y} We are being asked to develop S0 differently, using a different loop that does division of powers of 2 by powers of 2. It is helpful to examine the proof of the following to see which of the R0, R1, R2, R3, and R4 are used. {P /\ (R0: 1 <= d) /\ (R1: d*y <= r) /\ (R2: dd = d * y) /\ (R3: d is a power of 2) /\ (R4: r < 2 * d * y)} r,q := r-dd, q+d {P} Here's that proof. wp.(r,q := r-dd, q+d).(0 <= r /\ q*y + r = x) = {def} 0 <= r-dd /\ (q+d)*y + r-dd = x = {arithmetic} dd <= r /\ q*y + d*y + r - dd = x = {assuming R2} d * y <= r /\ q*y + d*y + r - d*y = x = {arithmethic} d * y <= r /\ q*y + r = x = {assuming R1 and P} true So R3 and R4 are purely for efficiency purposes; note that they are also involved with the particular solution that Cohen develops in 9.4. I think that having R3 and R4 around is causing confusion in this problem, so I propose that we solve the problem as follows. (We keep R0, because it is used for in the termination argument.) We consider the following annotated proof outline. {x >= 0 /\ y > 0} q,r := 0,x {invariant P: 0 <= r /\ q*y + r = x} ;do r >= y -> {P /\ r >= y} |[ var d, dd: int {P} ;S0 {P /\ (R0: 1 <= d) /\ (R1: d*y <= r) /\ (R2: dd = d * y)} ;r,q := r-dd, q+d {P} |] {P} od {P /\ ~(r >= y), hence R: 0 <= r /\ q*y + r = x /\ r < y} We are given the following predicates. R0: 1 <= d R1: d * y <= r R2: dd = d * y RR': R0 /\ R1 /\ R2 The problem says to choose for our invariant (deletion of R1 from RR') PP: R0 /\ R2 and for the guard (~R1) guard: d * y > r That is, we wish to solve for SS0 and SS in the following. {P} ;SS0 {P /\ PP: (R0: 1 <= d) /\ (R2: dd = d * y)} ;do d * y > r -> SS od {P /\ PP /\ ~(d * y > r), hence P /\ R0 /\ R1 /\ R2} In this solution, we will try to use divsision of a power of 2 by a power of two. We are free to introduce suitable other conjuncts to express what we are doing with powers of two. Hint: I think you'll find it helpful to think about how you could do division with a primitive division for digits, and then think of the binary expansion of x and y, in that context.