What Is a Loop Invariant? Proving Each Iteration Is Correct
A loop invariant is a statement that is true before or after every iteration. Establish it before the loop, preserve it through each update, and use it at termination to explain why the result is correct.
A loop invariant is a precise statement that remains true at a chosen point in every loop iteration. It connects the variables in the code to the meaning the algorithm is meant to preserve.
For a counting loop, the invariant can say that count equals the number of qualifying values in the prefix already processed. For binary search, it can say that if the target exists, it remains inside the current candidate interval. For two pointers, it can describe which values have already reached their final positions.
The three proof steps
First, establish the invariant. Show that it is true before the first iteration. A processed prefix is often empty at that point, so a counter initialised to zero has the required meaning.
Second, preserve the invariant. Assume it is true at the start of one iteration, then explain why the loop body makes it true for the next iteration. This step is where an off-by-one error or an update in the wrong order usually appears.
Third, use termination. When the loop condition becomes false, combine that fact with the invariant. If the processed prefix is now the whole array, the prefix count is the full answer. If a binary-search interval is empty, no candidate remains.
These steps prove correctness; they do not by themselves prove that the loop ends. Also identify a quantity that moves toward termination, such as an index that increases, a range that shrinks, or a pointer that never moves backward.
A counting example
The function below counts values strictly below a limit. At the start of iteration index, the invariant is:
countequals the number of values belowlimitat indexes from 0 throughindex - 1.
Press Run to execute this example. Use console.log to print a value.
Before the first iteration, no indexes have been processed and count is zero, so the invariant is established. During an iteration, the current value either qualifies and increases the count once, or does not qualify and leaves it unchanged. The statement is therefore preserved for the longer prefix.
When the loop ends, index === values.length. The processed prefix is the whole array, so the invariant says that count is the required total.
Invariants for ranges and data structures
An invariant should name the exact region or structure it describes. “The answer is correct so far” is too vague to test.
For binary search, say: if the target exists, an occurrence remains in the candidate interval. Every comparison must discard only indexes that cannot contain it.
For merge sort, say: the output contains the smallest consumed values in sorted order, and each pointer identifies the smallest unconsumed value on its side.
For a monotonic stack, say which indexes are unresolved and how their values are ordered from bottom to top. A later value can then pop exactly the entries it resolves.
Cost
Writing an invariant does not add runtime work. It is a reasoning tool for the loop already present. The loop's time still follows its iteration count, and its auxiliary space still follows the state it stores.
The invariant can make that cost easier to justify. If two pointers only move forward and each moves at most n times, the total is O(n), even when one pointer moves inside a nested while loop.
In the course
The course uses loop invariants in counting, binary search, sliding windows, merging, heaps, graph traversal, greedy scans, and dynamic programming. You do not need formal symbolic logic. State what the variables mean before an iteration, show that one update preserves that meaning, and explain what the statement gives you when the loop ends.
Common mistakes
An invariant is not a description of the next line. It must remain true across every iteration.
Do not omit the region: “the values are sorted” is weaker than “the consumed prefix of the result is sorted and contains exactly the consumed input values.”
Do not use the final answer as an assumption. The invariant should describe partial progress that the code can establish and preserve.
Termination needs its own argument. A true invariant does not prevent a loop whose pointers never advance.