# Invariant Proof of For Loops?

From CLRS (third edition, page 19), there is a footnote:

When the loop is a for loop, the moment at which we check the loop invariant just prior to the first iteration is immediately after the initial assignment to the loop-counter variable and just before the first test in the loop header.

Why is the checking moment specifically chosen to be after the initial assignment but before the first test? Note the excerpt is talking about proving correctness of algorithms using loop invariants.

-

The loop invariant probably involves the loop control variable. If so, it only makes sense to ask if the invariant is true, when the loop control variable is initialized. When the loop control variable is uninitialized, expressions that involve it are undefined.

Consider a simple example, a loop whose purpose is to determine whether all the elements of a (0-based) array $a$ are equal:

all_equal = true
for (i = 1; i < a.size; i++)
if a[i-1] ≠ a[i]
all_equal = false

Here the loop invariant is that $all\_equal$ is true if and only if the $a[k]$ are all equal for each $k$ with $0 \le k \le i$.

This is makes no sense at all unless the loop control variable $i$ has a well-defined value. Before the initialization, it doesn't. After the initialization, we have $i=1$, and the loop invariant is true.

-
Why do we have i = 0 instead of i = 1 after the initialisation? – Musa Al-hassy Apr 7 at 18:19
That was an error; I change my mind about the loop bounds. Thanks for pointing this out. – Mark Dominus Apr 7 at 19:21