4. Prove the correctness of the following loop using the provided pre and post conditions, and...

Transcribed Image Text:

4. Prove the correctness of the following loop using the provided pre and post conditions, and provided loop invariant. Require: A and B are positive integers, x = A, y = B and p =0 1: while y # 0 do 2: 3: 4: 5: 6: 7: 8: 9: 10: end if 11: end while Ensure: p = A. B r = y mod 2 if r = 0 then x = 2.x y := ydiv 2 end if if r = 1 then p=p+x Ynew Yold 1 Loop invariant: I(n): x y+p= A.B What does this loop compute? 4. Prove the correctness of the following loop using the provided pre and post conditions, and provided loop invariant. Require: A and B are positive integers, x = A, y = B and p =0 1: while y # 0 do 2: 3: 4: 5: 6: 7: 8: 9: 10: end if 11: end while Ensure: p = A. B r = y mod 2 if r = 0 then x = 2.x y := ydiv 2 end if if r = 1 then p=p+x Ynew Yold 1 Loop invariant: I(n): x y+p= A.B What does this loop compute?

Answer rating: 100% (QA)

To prove the correctness of the given loop with respect to the provided loop invariant and postcondition we need to show that 1 Initialization Before ... View the full answer