Consider the pseudo-code fragment, where m is a non-negative integer that has been initialized:

p = 0;
k = 0;
while (k < m)
    p = p + 2^k;
    k = k + 1;
end while

Which of the following is a loop invariant for the while statement? (A loop invariant is an assertion that is true each time the guard is evaluated.)

1. Ap = 2^k − 1 and 0 ≤ k < m
2. Bp = 2^(k+1) − 1 and 0 ≤ k < m
3. Cp = 2^k − 1 and 0 ≤ k ≤ m
4. Dp = 2^(k+1) − 1 and 0 ≤ k ≤ m

Pick an option to check yourself, or open the answer below.

Show answer & explanation

Correct answer: C. p = 2^k − 1 and 0 ≤ k ≤ m

Explanation

At each guard test p = 2⁰ + … + 2^(k−1) = 2^k − 1 (k = 0 gives p = 0). The guard is also evaluated one last time with k = m, so the bound must be 0 ≤ k ≤ m.

Note on the official key: the official key says option B. Official key gives (B), but p = 2^(k+1) − 1 already fails at the start (k = 0, p = 0), and k < m fails on the last guard test when k = m.