The following function computes $X^Y$ for positive integers X and Y.int exp(int X, int Y) { int res = 1, a = X, b = Y; while ( b != 0 ){ if ( b%2 == 0) { a = a*a; b = b/2; } else { res = res*a; b = b-1; } } return res; }Which one of the following conditions is TRUE before every iteration of the loop?

We need to find the loop invariant that holds true before every iteration of the while loop.

Initialization: Before entering the loop:

Checking option (C):

Thus, $X^Y = res \cdot a^b$ holds initially.

Maintenance: Assume $X^Y = res \cdot a^b$ holds at the start of an iteration.

• Case 1 ($b$ is even): The algorithm updates $a_{\text{new}} = a^2$, $b_{\text{new}} = b/2$, and $res_{\text{new}} = res$.

  $$res_{\text{new}} \cdot (a_{\text{new}})^{b_{\text{new}}} = res \cdot (a^2)^{b/2} = res \cdot a^b = X^Y$$

• Case 2 ($b$ is odd): The algorithm updates $res_{\text{new}} = res \cdot a$, $b_{\text{new}} = b - 1$, and $a_{\text{new}} = a$.

  $$res_{\text{new}} \cdot (a_{\text{new}})^{b_{\text{new}}} = (res \cdot a) \cdot a^{b-1} = res \cdot a^b = X^Y$$

In both cases, the relation $X^Y = res \cdot a^b$ is preserved for the next iteration.

Hence, (C) is the correct loop invariant.