Loop Invariant

A loop invariant is a condition that remains true before and after each iteration of a loop. It is a tool for explaining why loop-based algorithms are correct.

The invariant names what the loop has already accomplished.

Core Idea

A useful loop invariant has three parts. It is true before the loop starts. One loop iteration keeps it true. When the loop ends, the invariant helps prove the final result.

This is useful because many algorithms are loops that slowly grow a known-good region, shrink an unknown region, or maintain a summary of processed data.

A loop invariant is not a new algorithm. It is a sentence that makes the algorithm’s hidden reasoning explicit. Good invariants often mention the part of the input already processed and the meaning of the variables that summarize it.

Function Contract

prefix_sums(values) expects numeric values that can be added together.

It returns a list prefix with one extra leading zero. prefix[i] is the sum of the first i input values, so the sum of values[left:right] can be computed as prefix[right] - prefix[left].

Python Example

def prefix_sums(values):
    result = []
    running_total = 0
 
    for value in values:
        running_total += value
        result.append(running_total)
 
    return result

A loop invariant is: after processing i elements, running_total is the sum of the first i elements, and result contains the prefix sums for those i elements.

Step-by-Step Trace

For values = [3, 5, 2], the invariant develops like this:

• Before the loop, zero elements have been processed. running_total is 0, and result is empty.
• After processing 3, running_total is 3, and result is [3].
• After processing 5, running_total is 8, and result is [3, 8].
• After processing 2, running_total is 10, and result is [3, 8, 10].

At every point, running_total equals the sum of the processed prefix.

How To Use It

To write a loop invariant, ask what the loop has already made true.

For insertion sort, the invariant is that the prefix before the current index is sorted. For binary search, the invariant is that the target, if present, is still inside the current search interval. For a sliding window, the invariant may be that the window satisfies a certain constraint.

The invariant should connect directly to the final answer. If it does not help explain the result, it may be true but not useful.

Practice Signal

Loop invariants are especially helpful when a loop has moving boundaries, such as left and right, or when it maintains a partial structure, such as a sorted prefix, a heap, a current best answer, or a valid window.

If changing one line in a loop makes the result subtly wrong, an invariant can often reveal which promise was broken.

Common Confusions

A loop invariant is not just any condition inside a loop. It must stay true across iterations and help explain the result.

An invariant can be simple. It does not need to look formal to be useful. The main purpose is to make the reasoning explicit enough that the loop is not just trusted by intuition.

Another common mistake is stating the goal as the invariant. “The algorithm returns the correct answer” is not a useful invariant. A useful invariant explains what partial progress is correct during the loop.

When To Use It

Use a loop invariant when a loop maintains a subtle condition, such as a sorted prefix, a valid window, a current best answer, or a visited set. It is especially helpful when debugging off-by-one errors or explaining binary search.

Loop invariants are worth learning because many hard algorithm bugs are not syntax errors. They are broken assumptions about what a loop has preserved.

The Main Point

A loop invariant is the fact that makes a loop trustworthy. If the fact is true before the loop, preserved by each iteration, and strong enough at the end, the loop has a correctness argument.