Question

Write the loop invariant for the following program the computes quotients (q) and remainders (r) of “a” divided by ”d”. Then prove all three cases (Initialization, Maintenance, Termination). Assume “a” and “d” are positive integers.

r=a

q=0

while r>=d

            r=r-d

            q=q+1

Answer 1

r=a

q=0

while r>=d

         r=r-d

         q=q+1

A loop invariant is an expression that is true through all iterations. But it should also lead to the post-condition being true when the loop terminates

Intuitively, You would want the invariant to be r = a-q*d because that's what division is and that's what guarantees that you'll get the post-condition ( q=quotient, r=remainder) when the termination condition ( r < d ) is true.

• Loop Invariant:

  • Initialization: prior to the iteration of the loop we have r=a and q=0 and the loop invariant holds for that condition as
    r = a-0*d=a

  • Maintenance: To see that each iteration maintains the loop invariant, we check that if the loop has ran k times and in its k+1 iteration then the value of r will be r = a-k*d and according to our loop condition the value of q will be equal to no of iterations and hence its value will be equal to k, now if the condition for the loop still satisfies the value of r >= d and the loop variant still holds as r=a-k*d=a-q*d

  • Termination: At termination, r<d . By the loop invariant, the value of r = r-q*d which is at this time is equal to k and for k+1 the value of (k+1)*d > a and the value of r is lesser then the value of d and hence it is the reminder for this division algorithm and the value of q which is equal to k is the quotient of this division algorithm