the loop invariant

Think of climbing a ladder while balancing a tray. The useful thing to keep saying to yourself is not 'which rung am I on?' but 'the tray is still level.' If the tray is level when you start, and every single step keeps it level, then it is still level when you reach the top — no matter how many rungs there were. A loop invariant is exactly this kind of statement: a property about the program's variables that stays true on every pass of a loop, so that when the loop ends you can read off what was accomplished.

Formally, a loop invariant is a claim we attach to a loop and prove in three parts. Initialization: it is true just before the first iteration. Maintenance: if it is true before some iteration, it is still true before the next one (the body preserves it). Termination: when the loop exits, the invariant together with the exit condition tells us the loop did its job. The pattern mirrors induction: initialization is the base case, maintenance is the inductive step, and termination cashes out the conclusion. For example, in insertion sort the invariant is 'the prefix A[1..i-1] is sorted and contains the original first i-1 elements'; it holds before the loop, each step inserts A[i] keeping it true, and at the end the whole array is sorted.

Choosing a good invariant is the real art: too weak and it tells you nothing useful at the end; too strong and you cannot prove maintenance. The invariant must be strong enough that, combined with the exit condition, it implies what you want, yet exactly the kind of thing each iteration preserves. Once you have the right invariant, the correctness proof almost writes itself — which is why finding the invariant, not the proof bookkeeping, is where the thinking goes.