1.4 Loop Invariants

Loop invariants are the primary tool for reasoning about iterative algorithms. They formalize what remains true at each step of a loop and provide a bridge between local updates and global correctness. A loop invariant is not an observation after the fact. It is a design component that guides how the loop is written.

Problem

You need a reliable method to prove that a loop-based algorithm is correct, especially when the loop updates multiple variables and intermediate states are not obvious.

Solution

For a loop of the form:

initialize state

while condition:
  update state

use the following structure:

1. State an invariant that relates the current state to the problem.
2. Show the invariant holds after initialization.
3. Show each iteration preserves the invariant.
4. Show termination.
5. Show that when the loop ends, the invariant implies the required result.

The invariant should describe the meaning of the current state in terms of the portion of the input that has been processed.

Example: Prefix Maximum

max_value(A):
  best = A[0]

  for i = 1 to n - 1:
    if A[i] > best:
      best = A[i]

  return best

Invariant:

At the start of iteration i,
best is the maximum value in A[0..i-1].

Initialization:

Before the first iteration, i = 1 and best = A[0]. The invariant holds.

Maintenance:

At iteration i, compare A[i] with best. After the update, best becomes the maximum of A[0..i]. This matches the invariant for the next iteration.

Termination:

The loop ends when i = n. All elements have been processed.

Conclusion:

The invariant implies best is the maximum over the entire array.

Example: Two-Pointer Sum Search

Given a sorted array, determine if there exist two elements that sum to a target value.

two_sum_sorted(A, target):
  left = 0
  right = n - 1

  while left < right:
    s = A[left] + A[right]

    if s == target:
      return true
    else if s < target:
      left = left + 1
    else:
      right = right - 1

  return false

Invariant:

If a pair summing to target exists,
then it lies within indices [left, right].

Initialization:

Initially, [left, right] spans the entire array, so the invariant holds.

Maintenance:

If the sum is too small, increasing left removes pairs that cannot reach the target. If the sum is too large, decreasing right removes pairs that exceed the target. In both cases, no valid solution is discarded.

Termination:

The loop ends when left >= right. No candidate pairs remain.

Conclusion:

If the algorithm does not return true, then no valid pair exists.

Designing Loop Invariants

A useful invariant has three properties:

It describes a meaningful subset of the problem
It connects directly to variables in the loop
It is preserved by each update

Common patterns include:

Prefix processing

State describes the result for A[0..i-1].

Search space reduction

All valid solutions lie within the current interval.

Accumulation

State stores the result of combining processed elements.

Partitioning

The array is divided into regions with known properties.

Strength of Invariants

An invariant should be strong enough to imply the final result, but not so strong that it becomes difficult to prove preservation.

Weak invariant example:

best is some value from the array

This is true but useless.

Strong invariant example:

best is the maximum of the processed prefix

This directly leads to the correct result.

Termination Conditions

Termination is often tied to a counter or pointer that moves monotonically:

Index increases until a bound
Interval shrinks until empty
Remaining work decreases each step

Termination must be explicit. An invariant alone does not guarantee the loop ends.

Common Pitfalls

An invariant that changes meaning across iterations leads to incorrect reasoning. The invariant must have the same interpretation at every step.

An invariant that ignores part of the state often fails during updates. If multiple variables interact, the invariant must describe their relationship.

Updating variables without checking the invariant leads to subtle bugs. Every assignment should be justified by preservation.

Takeaway

A loop invariant gives a precise meaning to the state of a loop at every iteration. It allows you to prove correctness by showing that initialization, maintenance, and termination together imply the required result.