TL;DR: When the loop exits, i = n. Claim remains true (even after i increments to i+1, equaling n, and the body is not executed).
Maybe the definition of madness is repeatedly explaining the same concept over and over.
I neglected an operation that participates in the framing of the loop invariant: the incrementing of the loop variable. Its mention is done in passing; I place it here to make it explicit. Here is code to find the maximum of a 0-based array:
currentMax <- A
for i = 1; i < n; i++
if currentMax < A[i] then
currentMax = A[i]
The claim is at the beginning of iteration i, the variable currentMax will have the maximum value of the first i elements in the array A. The author goes on to say “if this claim is true, it will be true after it for i+1.” What does that mean?
(I noticed we don’t really look at the logic of the loop body; for our purposes, we are concerned with instruction counts versus correctness.)
It’s important for the claim to remain true after i+1 because when i = n, the loop ends and the body is never executed. Our loop’s last moments:
at the beginning of the (n-1)th iteration,
currentMax is the maximum value of the first (n-1) elements of A
(i = i + 1)
at the beginning of the nth iteration,
currentMax is the maximum value of the first n elements of A
(i < n is false because i = n, so exit)
Why does it “remain true?” I took the quote out of context; it should be “remains true after [it] for i+1.” Substituting for the “for” (because it is a loop keyword),
… remains true after [it] when i is incremented by one.
Which pieces of the claim remain true?
before the i-th iteration TRUE
during the body TRUE
after the body TRUE
incrementing i TRUE
before the (i+1)th iteration (TRUE)
I forget what the loop invariant is for: is it to demonstrate that the algorithm is true? Is it to conceptualize its instructions as discrete operations? Seeing that the next step is to total them to determine the function f(n) to find growth rate, it is less debugging and more… something else. I will have to read some more.