Correctness: Loop Invariants & Induction — Algorithms Course

What you'll learn

An algorithm that works on your three test cases might still be wrong. This module is about proving an algorithm correct — for every input — using two timeless tools: the loop invariant and mathematical induction.

By the end you'll be able to:

State what it means for an algorithm to be correct
Find and use a loop invariant
Prove a recursive algorithm correct by induction
Argue that an algorithm terminates

What correctness means

An algorithm is correct if, for every input satisfying its precondition, it halts and produces output satisfying its postcondition. "Sort" has the precondition "a is a list of comparable items" and the postcondition "a is a permutation of the input, in non-decreasing order." Testing can reveal bugs; only a proof can guarantee their absence.

Loop invariants

A loop invariant is a statement that stays true every time the loop's top is reached. Prove three things about it and you've proved the loop correct — it's induction in disguise:

The three obligations of a loop invariant

Initialization

The invariant is true before the loop's first iteration.

Maintenance

If it's true before an iteration, it's still true after.

Termination

When the loop ends, the invariant gives the result you want.

A worked proof

Take find_max. Claim the invariant: at the top of the loop, best equals the maximum of nums[0..i] (the elements seen so far).

Language

find_max.py

def find_max(nums):
    best = nums[0]
    # invariant: best == max(nums[0..i])
    for i in range(1, len(nums)):
        if nums[i] > best:
            best = nums[i]
    return best   # i has reached the end -> best == max(nums)

Initialization: before the loop, best = nums[0], which is indeed the max of nums[0..0].
Maintenance: each iteration sets best to the larger of the old best and nums[i] — the max of nums[0..i]. ✓
Termination: the loop ends when i passes the last index, so best is the max of the whole list. ∎

Key idea

Choosing the right invariant is the whole art. A good invariant is exactly the fact you need at loop exit to reach the postcondition.

Induction & recursion

Recursive algorithms are proven by induction: show the base case is correct, then assume the recursive calls (on smaller inputs) are correct and show the current call is too. Because each call shrinks the input toward the base case, the assumption is always safe — this is strong induction. It's the same logic as the loop invariant, just phrased for recursion.

Termination

Correctness includes halting. The usual argument names a quantity — a variant — that strictly decreases each step and can't drop below a floor. In find_max, the number of remaining indices decreases each iteration and stops at zero. In recursion, the input size shrinks toward the base case. No infinite descent is possible, so the algorithm terminates.

Note

Invariant = a quantity that stays true; variant = a quantity that strictly decreases. Together they prove "correct and finishes."

Recap & quick check

Key takeaways

Correct = for every valid input, the algorithm halts with output meeting its postcondition.
A loop invariant is proven in three steps: initialization, maintenance, termination.
The right invariant is exactly the fact you need at loop exit.
Recursive algorithms are proven correct by (strong) induction.
Termination is shown with a variant — a quantity that strictly decreases to a floor.

Quick check

1. What are the three parts of a loop-invariant proof?

2. Why isn't testing enough to guarantee correctness?

3. How are recursive algorithms usually proven correct?

4. What is a 'variant' used to show?

You can now reason about cost and correctness. Let's meet the structures every algorithm leans on. Next up: Module 5 — The Data Structures You'll Rely On.