# 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:

```text
initialize state

while condition:
  update state
```

use the following structure:

```text
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

```text
max_value(A):
  best = A[0]

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

  return best
```

Invariant:

```text
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.

```text
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:

```text
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**

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

**Search space reduction**

```text
All valid solutions lie within the current interval.
```

**Accumulation**

```text
State stores the result of combining processed elements.
```

**Partitioning**

```text
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:

```text
best is some value from the array
```

This is true but useless.

Strong invariant example:

```text
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.