Consider the following pseudo-code fragment, where m is a non-negative integer…

Concept: A loop invariant is an assertion that holds every time the while-guard is tested — including the very first test and the final test that ends the loop. To prove a candidate is an invariant you check three things in the abstract: (1) Initialization — it holds before the first guard test; (2) Maintenance — if it holds before an iteration and the body runs, it still holds before the next guard test; and (3) Bound coverage — the range on the counter must include the value the counter has at the terminating guard test (when the guard is false), not stop one short.

Application: Here the body adds 2k to p on each pass, so after the counter has reached value k the accumulated sum is 20 + 21 + … + 2k-1 = 2k − 1. Trace the three obligations:

1. Initialization: before the first test p = 0 and k = 0, and 20 − 1 = 0 = p, so p = 2k − 1 holds; also 0 ≤ k ≤ m since m is non-negative.

2. Maintenance: assume p = 2k − 1 at a guard test with k < m. The body sets p ← (2k − 1) + 2k = 2k+1 − 1, then k ← k + 1, so p = 2k − 1 holds again for the new k.

3. Bound coverage: the guard is tested one last time when k = m (and is false), so the counter range must include k = m. Hence the bound is 0 ≤ k ≤ m, not 0 ≤ k < m.

Cross-check: Take m = 3. Successive guard tests see (p,k) = (0,0), (1,1), (3,2), (7,3); each satisfies p = 2k − 1, and the last test has k = 3 = m — only the inclusive bound 0 ≤ k ≤ m admits it. So the invariant is p = 2k − 1 with 0 ≤ k ≤ m.