Using a Loop Invariant to Help Think About a Program

In the previous article, the closest thing to an explanation or definition of a loop invariant is, "We can make it less so by writing down a specific claim that applies to our particular loop. Such a claim is called a loop invariant." Not a very good description, and he doesn't try to do any better elsewhere.

I ended up having to do a bunch of googling after reading the articles to piece together what is trying to be explained, since I had never heard of loop invariants in that terminology either.

Simply put, a loop invariant is a condition or set of conditions that is true through the loop. This makes it akin to inductive proofs. The loop invariant must prove true for n and n+1 for it to be true for the entirety of the loop. Noting how similar this is to inductive reasoning, you can apply an inductive proof to a loop invariant to prove it.

The easiest way I've seen to explain it is in the body of the executing loop you ask yourself, "What has the loop done so far." An answer to that question should yield a loop invariant.