5.2 Correctness and Loop Invariants

Section 5.1 taught us to write and trace algorithms. A successful trace proves only that one input worked. An algorithm specification usually makes a universal claim:

Chapter 3 gave us methods for universal proofs and counterexamples. We now apply those methods to programs.

Preconditions and postconditions define the promise

A precondition states what must be true before an algorithm begins. A postcondition states what must be true when it finishes.

Consider:

DIVIDE-SUM(a, b, n)
    return (a + b) / n

A necessary precondition is $n\ne0$. A possible specification is:

• precondition: $a,b,n\in\mathbb R$ and $n\ne0$;

• postcondition: the returned value equals $(a+b)/n$.

The algorithm is not required to behave meaningfully for inputs that violate its precondition unless the specification says how to handle them.

For the summation algorithm

SUM-TO(n)
    total ← 0
    for i ← 1 to n
        total ← total + i
    return total

we may specify:

• precondition: $n$ is a nonnegative integer;

• postcondition:

The index $j$ in the summation is a local mathematical name. We use it to avoid confusing the whole sum with the algorithm’s changing loop variable $i$.

Partial correctness and total correctness

Two obligations are hidden inside “the algorithm is correct.”

Partial correctness means:

Termination means:

Total correctness combines them:

An infinite loop could satisfy partial correctness vacuously because it never returns a wrong answer—it never returns at all. That is why termination must be proved separately.

Why loops need a new proof idea

An if statement has finitely many branches, so we can prove each case. A loop may execute any number of times depending on its input. We need one statement that describes every iteration.

A loop invariant is a proposition that is true:

1. before the first iteration;

2. after every completed iteration;

3. therefore, when the loop stops.

The word “invariant” means that the statement remains true even though variable values change.

An invariant is not necessarily the final postcondition. It describes the progress already completed and the work that remains.

Discovering an invariant for summation

Return to:

total ← 0
for i ← 1 to n
    total ← total + i
return total

Immediately before the iteration with current value $i$, the algorithm has already added

A useful invariant is

We now prove it using three obligations.

1. Initialization

Before the first iteration, $i=1$ and $total=0$. The sum of integers from $1$ through $0$ is an empty sum, defined as $0$. Therefore

The invariant holds before the loop starts.

2. Maintenance

Assume the invariant holds before an arbitrary iteration with value $i$:

The body performs

After the update,

The loop then advances to $i+1$. Written using the new loop value, the invariant becomes

Thus, if the invariant is true before an iteration, it remains true before the next one.

3. Termination connection

After the final iteration $i=n$, the loop variable has advanced past $n$. The invariant tells us

which is the required postcondition.

The proof pattern is:

This resembles mathematical induction from Chapter 3. Initialization is the base case, and maintenance is the inductive step over loop iterations.

Advance a summation machine one iteration at a time while choosing among candidate invariants. A force field remains stable only when the assertion matches every visible state; false invariants crack at the first counterexample, and the exit state must unlock the postcondition.

Proving termination with a decreasing measure

For a while loop, identify a nonnegative integer quantity that decreases on every iteration. This is often called a variant or ranking function.

Consider Euclid’s repeated-subtraction procedure for positive integers $a,b$:

while a ≠ b
    if a > b
        a ← a - b
    else
        b ← b - a
return a

While $a\ne b$, both values remain positive. The measure

is a positive integer. Each iteration subtracts the smaller value from the larger, so $V$ strictly decreases by a positive amount.

A strictly decreasing sequence of positive integers cannot continue forever. Therefore the loop terminates.

To use a termination measure correctly, prove:

1. it belongs to a set with no infinite strictly decreasing chain, such as the nonnegative integers;

2. it decreases on every iteration that continues the loop;

3. it cannot decrease forever without reaching an exit state.

Simply saying “the variables get smaller” is not enough if a variable could become negative or oscillate.

Correctness of linear search

Suppose an array

contains $n$ items. The notation $A[i]$ means the item stored at index $i$. Indices begin at $0$ and end at $n-1$.

The goal is to return an index holding target $t$, or return $-1$ if $t$ is absent.

LINEAR-SEARCH(A, t)
    for i ← 0 to length(A) - 1
        if A[i] = t
            return i
    return -1

A useful loop invariant is:

> Immediately before checking index $i$, the target does not occur at any index $0,1,\ldots,i-1$.

Initialization

Before $i=0$, no earlier index exists. The claim about the empty prefix is true.

Maintenance

If $A[i]\ne t$, then after checking index $i$, the target is absent from indices $0$ through $i$. The invariant is ready for the next value $i+1$.

If $A[i]=t$, the algorithm returns $i$, and the output is correct.

Exit

If the loop finishes without returning, every valid index has been checked and differs from $t$. Returning $-1$ is correct.

Termination

The for loop checks at most $n$ indices, so it terminates.

Together these arguments prove total correctness.

Testing finds bugs; proof rules them out universally

Testing and proof have different jobs.

• A passing test shows that one chosen input behaves correctly.

• A failing test is a counterexample and proves the implementation is incorrect.

• A proof establishes correctness for all inputs satisfying the precondition.

Small and boundary inputs are especially valuable for finding bugs:

• an empty array;

• an array of length $1$;

• the target at the first or last index;

• the target absent;

• duplicate target values.

Consider this buggy search:

for i ← 0 to length(A) - 2
    if A[i] = t
        return i
return -1

It never checks the last index. The input

is a counterexample: the algorithm returns $-1$ even though the target occurs at index $2$.

Other bugs may read beyond the array or fail to advance the index, producing an invalid access or nontermination. A good adversarial test is chosen to activate the suspected weakness.

Investigate several nearly correct search agents. Build adversarial arrays, run animated execution, and capture one of four failure types: wrong answer, missed boundary, invalid access, or nontermination. Then patch the responsible line and rerun the same counterexample.

Section bridge

Correctness asks whether an algorithm returns the right answer and terminates. Two correct algorithms may still require very different amounts of work. Section 5.3 introduces a cost model, counts operations as input size grows, and compares growth rates without being distracted by one machine’s speed.