Correctness

A program can compile, finish quickly, and still be wrong. It may fail only for an empty input, for duplicate values, after integer overflow, or for an arrangement no test author imagined. Algorithms therefore begin one step before code: state exactly what must be computed, state the conditions under which the promise is made, then justify that every permitted execution fulfills that promise.

This chapter develops the language for doing that. The goal is not formalism for its own sake. A good specification exposes ambiguity before implementation; a good invariant guides the loop you should write; a good proof identifies the assumptions under which an optimization is safe. Correctness reasoning is a design tool first and a verification tool second.

Problem Specification

An algorithmic problem describes a relationship between admissible inputs and acceptable outputs. An instance is one concrete input. An algorithm is a finite procedure intended to produce an acceptable output for every admissible instance.

Consider the problem maximum index:

Given a nonempty finite array a[0..n-1] of integers, return an index p such that a[p] >= a[i] for every valid index i.

This sentence contains three parts that should be made explicit whenever the details matter.

Inputs

• an integer array a;
• its length n;
• the elements are representable as C int values.

The input is not merely “an array.” Its size and representation are part of what the implementation receives. In mathematical pseudocode, the length may be implicit; in C, it usually is not.

Outputs

The output is an index, not the largest value. If the maximum appears more than once, any maximum index satisfies the stated problem. If the caller requires the first maximum, that is a different specification:

A correct algorithm for the first specification can be incorrect for the second. Tie behavior is not a cosmetic implementation detail when callers observe it.

Constraints

The phrase nonempty is load-bearing. Without it, no valid index exists. Other problems may constrain values to be nonnegative, require an array to be sorted, forbid cycles in a graph, or guarantee that arithmetic fits its chosen type. Every correctness claim is conditional on these constraints.

Ask “what should happen?” before “how will I compute it?” If two sensible readers could disagree about empty input, ties, overflow, mutation, or error reporting, the contract is unfinished.

Algorithm Specification

The contract of an algorithm is commonly divided into a precondition and a postcondition.

• A precondition describes what must be true when the algorithm starts.
• A postcondition describes what the algorithm guarantees if it starts in a state satisfying the precondition and terminates normally.

For a first-maximum implementation:

MAX_INDEX(a, n)
Pre:  n > 0 and a[0..n-1] is readable
Post: returns p such that
      0 <= p < n,
      a[p] >= a[i] for every 0 <= i < n, and
      no index smaller than p contains a[p]

A C interface can make failures explicit rather than relying on an undocumented precondition:

#include <stdbool.h>
#include <stddef.h>

bool max_index(const int a[], size_t n, size_t *out_index) {
    if (a == NULL || out_index == NULL || n == 0) {
        return false;
    }

    size_t best = 0;
    for (size_t i = 1; i < n; ++i) {
        if (a[i] > a[best]) {          /* strict > preserves the first maximum */
            best = i;
        }
    }

    *out_index = best;
    return true;
}

The Boolean result extends the contract:

• on true, *out_index satisfies the postcondition;
• on false, the function makes no success claim and does not write through out_index.

Changing > to >= would preserve “returns a maximum” but would change “first maximum” into “last maximum.” The proof tells us exactly which line controls the tie policy.

Assertions

An assertion is a logical statement about a program state at a particular point. The notation

is a Hoare triple. It says that if precondition P is true before statement or algorithm A starts, and A terminates, then postcondition Q is true afterward. By itself this is a partial-correctness claim; a total-correctness claim additionally proves that A terminates from every state satisfying P.

Assertions make local reasoning possible. Three basic composition ideas are enough for many hand proofs:

• Sequence: if {P} A {R} and {R} B {Q}, then {P} A; B {Q}. The intermediate assertion R connects the two pieces.
• Choice: to prove an if statement, prove the desired postcondition from both P && condition through the true branch and P && !condition through the false branch.
• Assignment: to make a desired assertion true after x = expression, determine what must have been true before replacing x by expression. For example, to establish x > 10 after x = y + 1, it is enough to know y + 1 > 10 before the assignment.

Assertions can be written beside the maximum loop:

{ n > 0 and a[0..n-1] is readable }
best = 0
i = 1
{ best is the first maximum index of a[0..i-1] }

while i < n:
    { invariant and i < n }
    if a[i] > a[best]:
        best = i
    i = i + 1
    { best is the first maximum index of a[0..i-1] }

{ invariant and i == n }
{ best is the first maximum index of a[0..n-1] }

This is more than annotation after the fact. Starting with the final assertion and asking what must remain true before every iteration often reveals the variables, comparison direction, and boundary representation the implementation needs.

Sorting Contract

Some algorithms need a postcondition with several independent clauses. “The output is sorted” is not a complete sorting specification. For an input sequence A and output sequence B, a comparison sort normally promises:

1. Order: B[i] <= B[i+1] for every adjacent valid pair.
2. Preservation: B is a permutation of A; every input record occurs in the output with the same multiplicity.
3. Location: the contract says whether B is a separate result or the input storage is mutated in place.
4. Stability, when promised: if two input records have equal keys and the first precedes the second in A, their relative order remains the same in B.

The preservation clause prevents an implementation from returning [-infinity,-infinity,...], which is ordered but discards the data. For bounded integer keys, preservation can be expressed by equal frequency counts. For arbitrary records, one can tag every input record with a unique identity and require that the output contain exactly the same identities.

Stability is observable only when equal-key records have other distinguishable fields. The integer sequences [2,2] and [2,2] do not reveal whether records were reversed, but [(2,"A"),(2,"B")] does. Specifications should describe records at the level the caller observes rather than at the level convenient for one example.

Multi-clause contracts guide proofs as well. Merge sort needs one argument that the merge output is ordered and another that each input item is copied exactly once. If stability is required, a third argument explains why ties are taken from the left run first. Proving only ordering leaves two-thirds of the intended behavior unjustified.

Correctness Types

Correctness has two logically separate obligations.

Partial Correctness

An algorithm is partially correct if:

whenever its precondition holds and it terminates, its postcondition holds.

The qualification matters. This program is partially correct for “return zero” but not useful:

int zero_forever(void) {
    for (;;) {
        /* never returns a wrong value—or any value */
    }
    return 0;
}

Partial correctness proves that an obtained answer is right. It does not prove that an answer will be obtained.

Total Correctness

An algorithm is totally correct if it is partially correct and terminates for every input satisfying its precondition.

The standard proof plan is therefore:

1. Safety: prove that the postcondition holds if the algorithm stops.
2. Progress: prove that the algorithm must stop.

Separating safety from progress is useful beyond sequential algorithms. “Nothing bad happens” and “something good eventually happens” are different questions in concurrent programs, network protocols, and distributed systems as well.

Loop Invariants

A loop invariant is a statement about program state that is true whenever control reaches a particular point in a loop—usually immediately before the condition is tested. A useful invariant connects the work already completed with the final postcondition.

For max_index, use:

At the start of the iteration with index i, best is the smallest index containing a maximum of the processed prefix a[0..i-1].

This statement is precise enough to prove the first-maximum policy, not merely the maximum value.

Initialization

Before the first iteration, i = 1 and best = 0. The processed prefix contains only a[0]; index 0 is trivially its first maximum. The invariant holds.

Maintenance

Assume the invariant holds at the start of an iteration.

• If a[i] > a[best], the new element is strictly larger than every element in the old prefix. Assigning best = i makes it the unique maximum of the enlarged prefix.
• If a[i] <= a[best], the old maximum remains a maximum. When equality holds, leaving best unchanged preserves the smallest maximum index.

In either branch, the invariant holds for the prefix a[0..i], which is exactly the processed prefix at the next iteration.

Termination

The loop ends when i == n. Substitute that fact into the invariant: best is the first maximum index of a[0..n-1], the entire array. This is the postcondition.

The three-part proof mirrors mathematical induction:

Finding Invariants

An invariant should be strong enough to imply the result at termination but weak enough to establish initially. Useful ways to discover one include:

1. Turn the postcondition into a prefix claim. “The result is correct for the whole array” becomes “the current result is correct for the part already processed.”
2. Name the unexplored region. Binary search maintains that a target, if present, remains inside the current interval.
3. Describe preserved structure. In insertion sort, the processed prefix remains sorted and contains exactly the original prefix elements.
4. Track conservation. In flow algorithms, net flow is conserved at every internal vertex.
5. Track a boundary. Two-pointer algorithms often maintain that everything outside the pointers is already classified.

A statement such as “the loop has processed i items” is usually true but too weak: it does not say what was accomplished by processing them.

Maximum Trace

Trace max_index on [4, 9, 3, 9, 7]:

The trace is evidence for this instance. The invariant proof covers every finite nonempty array, including ones we did not trace.

Recursive Correctness

Recursive algorithms are usually proved by strong induction on a measure of input size. The induction hypothesis is not a leap of faith: it states precisely that every smaller recursive call returns a correct answer, which is what the recursive case needs.

Consider Euclid’s algorithm for the greatest common divisor of nonnegative integers:

unsigned gcd(unsigned a, unsigned b) {
    if (b == 0U) {
        return a;
    }
    return gcd(b, a % b);
}

Specification

Pre:  a and b are nonnegative, and not both zero
Post: returns the greatest positive integer dividing both a and b

The mathematical insight is:

Why? Write a = qb + r, where r = a mod b.

• Any number dividing both a and b divides a - qb = r.
• Any number dividing both b and r divides qb + r = a.

Therefore the two pairs have exactly the same common divisors and hence the same greatest one.

Inductive proof. Use b as the measure.

• Base case b = 0: the function returns a; every positive divisor of a divides 0, so gcd(a,0)=a.
• Recursive case b > 0: 0 <= a % b < b. By the induction hypothesis, the recursive call correctly computes gcd(b, a % b). By the identity above, that value is gcd(a,b).

Termination. In every recursive call, the second argument becomes a % b, which is a nonnegative integer strictly smaller than the previous positive second argument. A strictly decreasing sequence of nonnegative integers cannot continue forever. Euclid’s algorithm is totally correct.

Trace gcd(252, 105):

gcd(252, 105)
gcd(105,  42)    because 252 mod 105 = 42
gcd( 42,  21)    because 105 mod 42  = 21
gcd( 21,   0)    because 42  mod 21  = 0
returns 21

Notice the division of labor: the number-theoretic identity proves the recursive answer is correct; the decreasing remainder proves recursion ends.

Proof Obligations

Different problem types divide correctness into different claims. Naming them prevents a proof from establishing one property while silently assuming another.

For a decision algorithm, two directions are required:

• soundness: whenever the algorithm answers yes, the instance really is a yes-instance;
• completeness: whenever the instance is a yes-instance, the algorithm answers yes.

A subset-sum search is sound if every accepted branch records distinct input choices whose sum is the target. It is complete if its branches cover every possible subset. Showing only that a returned subset has the right sum does not prove the algorithm will find one whenever one exists.

For a construction algorithm, prove feasibility of the returned object and, when relevant, that failure is reported only when no feasible object exists. A path finder must show that consecutive returned vertices are joined by edges, that endpoints are correct, and that an unreachable report is justified.

For an optimization algorithm, add optimality. A minimum spanning tree proof, for example, needs all of the following:

1. returned edges belong to the input graph;
2. they span the required vertices and form a tree;
3. no other spanning tree has smaller total weight.

The first two establish feasibility, not minimum weight. Greedy exchange and cut arguments usually address the third obligation; invariants about components address the first two.

For an enumeration algorithm, prove coverage and uniqueness in addition to validity. A permutation generator must emit only permutations, emit every permutation, and avoid duplicates. Its cost must also include the output volume, which can dominate internal search.

Approximation and randomized algorithms modify rather than remove these obligations. An approximation algorithm proves feasibility and a stated ratio to optimum. A Monte Carlo decision algorithm states which direction may err and bounds that error probability. Clear proof obligations turn a vague claim that an algorithm “works” into a checklist tied directly to its specification.

Proof Techniques

Proofs are structured explanations. Different algorithms expose different structures, so no single template fits everything.

Direct Proof

A direct proof starts from the precondition and derives the postcondition using definitions and known facts. The proof of the GCD identity above is direct: divisibility facts are transformed algebraically until equality of common-divisor sets follows.

Direct proofs work well for one-pass formulas, algebraic transformations, and reductions that preserve a clearly defined property.

Mathematical Induction

Use induction when the algorithm or data has a recursive or cumulative shape.

• Loop invariants are induction over the number of iterations.
• Recursive correctness is induction over input size or structural depth.
• Divide-and-conquer proofs assume correctness on smaller pieces and prove that the combine step creates a correct whole.

The induction measure must be well founded. “Assume it works for the recursive call” is incomplete until you show that call is genuinely smaller under a measure that cannot decrease forever.

Contradiction Proofs

A proof by contradiction assumes the desired claim is false and derives an impossibility.

For example, suppose an algorithm reports m as the minimum element after checking every item and maintaining the invariant that m is the smallest seen. Assume the returned m is not globally minimum. Then some array item x < m exists. That item was processed; maintenance would have replaced m by x or an even smaller value. Thus m could not remain larger than x, contradicting the final state.

Contradiction is especially natural for optimality (“assume a better solution exists”), cycles, lower bounds, and greedy-choice proofs.

Counterexamples

A universal claim—“this algorithm works for every valid input”—is disproved by one valid counterexample. A strong counterexample is:

• valid under the stated precondition;
• as small as possible;
• targeted at the exact unsupported assumption;
• accompanied by a trace showing the wrong result.

Consider the tempting algorithm “return the first array item larger than its predecessor as the maximum.” [1, 3, 2, 9] is a counterexample: it returns 3, although the maximum is 9. Ten successful tests cannot prove a universal claim; one such trace refutes it.

When testing a proposed greedy strategy, deliberately search for small instances where a locally attractive decision consumes a resource needed by a better global solution. When testing a boundary algorithm, try empty, singleton, duplicated, all-equal, and extreme-value inputs.

Termination Proofs

To prove a loop or recursion terminates, identify a variant (also called a ranking function): a value drawn from a well-founded set that decreases strictly on every iteration while remaining bounded below.

For a half-open lower-bound search:

#include <stddef.h>

size_t lower_bound_int(const int a[], size_t n, int target) {
    size_t lo = 0;
    size_t hi = n;
    while (lo < hi) {
        size_t mid = lo + (hi - lo) / 2;
        if (a[mid] < target) {
            lo = mid + 1;
        } else {
            hi = mid;
        }
    }
    return lo;
}

the candidate count hi - lo is a natural variant. If a[mid] < target, setting lo = mid + 1 removes mid and everything below it. Otherwise hi = mid removes everything above or equal to the old mid boundary. Each branch strictly reduces hi - lo without unsigned underflow. Updating lo = mid instead can leave a two-element interval unchanged, exposing a possible infinite loop.

Termination is only half of the lower-bound proof. Its full invariant is:

every index j < lo satisfies a[j] < target,
every index j >= hi satisfies a[j] >= target, and
the first qualifying index, if one exists, lies in [lo,hi).

Initially, [lo,hi)=[0,n), so neither excluded region contains an index and the claims are vacuously true. When a[mid] < target, sorted order implies every index through mid also fails, making mid + 1 the correct new lower boundary. Otherwise mid may be the first qualifying position, so it must remain in the candidate interval; assigning hi = mid does exactly that. At termination lo == hi, the candidate interval is empty. Everything below lo fails and everything at or above lo qualifies, making lo the first qualifying index, or n if none qualifies.

This proof explains three implementation details that otherwise look arbitrary: a half-open interval permits n as a valid “not found” answer, the false branch retains mid, and the true branch discards it. A boundary-search bug often comes from mixing a proof for one interval convention with updates from another.

Common variants include:

• remaining unprocessed elements;
• distance between two indices;
• height of a remaining tree;
• size of a recursive subproblem;
• number of unsettled vertices;
• lexicographic pairs such as (rows remaining, columns remaining).

“The loop obviously ends” is not a proof when an update can preserve or increase the variant through overflow, rounding, or a missed branch.

Correctness Failures

Correctness claims are only as honest as their model. Check these boundaries explicitly:

Invalid Inputs

An algorithm can require a precondition, return an error, or define behavior for the exceptional case. What it must not do is silently dereference an empty array while its documentation implies all inputs are supported.

Arithmetic Overflow

Mathematical integers are unbounded; C integers are not. The expression dist[u] + weight can overflow even when the mathematical shortest path is well defined. A production contract must constrain values, use a wider type, or check before arithmetic.

Overflow can invalidate a proof at the exact step where algebra assumes ordinary integer laws. In mathematical integers, x + 1 > x; for a signed C int, evaluating INT_MAX + 1 has undefined behavior. In unsigned arithmetic it wraps to zero. A termination proof that says “the unsigned counter strictly increases until it reaches the bound” must also establish that the counter cannot wrap before reaching that bound.

Floating Arithmetic

Real-number identities do not transfer automatically to floating-point arithmetic. Addition is not associative: (a + b) + c can differ from a + (b + c) after rounding. NaN compares unequal even to itself, signed zeros can carry different behavior in some operations, and an accumulated error can change a branch decision.

A numerical contract should specify acceptable error, not demand exact equality to an ideal real result unless exactness is actually guaranteed. Typical postconditions use an absolute tolerance, a relative tolerance, or a problem-specific residual such as |Ax-b|. The proof must then include an error analysis compatible with the chosen representation.

Representation Mismatch

An algorithm proved for a directed graph may fail on an undirected representation that stores each edge twice. An algorithm proved for simple graphs may need adjustment for parallel edges or self-loops. Data representation belongs in the assumptions of the proof.

Nondeterminism

When several outputs are valid—multiple topological orders or minimum spanning trees, for example—the postcondition should describe the property every acceptable output satisfies, not one exact sequence seen in a sample run.

Randomized algorithms require an additional quantifier. A Las Vegas algorithm, such as randomized quicksort, always returns a correct result but has a random running time. Its correctness proof covers every sequence of random choices; probability appears only in the cost analysis. A Monte Carlo algorithm has a bounded probability of error or one-sided failure. Its contract must state that probability and what randomness it is measured over—for every fixed valid input, over the algorithm’s internal random choices. Saying merely that it “usually works” is not a correctness statement.

Mutation and Aliasing

If an algorithm rearranges input in place, its contract must say so. If output aliases input, a proof that assumes independent buffers may not describe the actual program.

Testing Limits

Testing and proof answer different questions.

• A proof establishes a mathematical claim under an abstract model and stated assumptions.
• Testing checks that a concrete implementation behaves as expected on selected executions in a concrete environment.

Both are necessary. A valid proof of insertion sort does not prove that a particular C implementation lacks an out-of-bounds write. A million passing tests do not prove a universal claim over an unbounded input domain.

Useful Test Classes

For an array algorithm, include:

1. the smallest valid input;
2. boundary-invalid inputs if the interface reports errors;
3. already structured and reverse-structured data;
4. all-equal and duplicate-heavy data;
5. extreme representable values;
6. randomized cases compared with a simple trusted reference;
7. adversarial inputs derived from the algorithm’s assumptions.

Properties as Oracles

Sometimes the exact answer is expensive to write down, but a property is easy to check. After sorting:

• the output is nondecreasing;
• the output is a permutation of the input;
• if stability is promised, equal keys preserve original order.

Checking only the first property misses an implementation that returns an array full of the minimum value. Correct postconditions often make excellent test oracles precisely because they describe all necessary properties.

Complete Proof

The following C17 program implements max_index, tests representative cases, and checks the postcondition independently. The checker is deliberately simple; it is not the proof, but it is useful implementation evidence.

#include <assert.h>
#include <stdbool.h>
#include <stddef.h>
#include <stdio.h>

static bool max_index(const int a[], size_t n, size_t *out_index) {
    if (a == NULL || out_index == NULL || n == 0) {
        return false;
    }

    size_t best = 0;
    for (size_t i = 1; i < n; ++i) {
        if (a[i] > a[best]) {
            best = i;
        }
    }
    *out_index = best;
    return true;
}

static bool is_first_maximum(const int a[], size_t n, size_t p) {
    if (a == NULL || n == 0 || p >= n) {
        return false;
    }
    for (size_t i = 0; i < n; ++i) {
        if (a[i] > a[p]) {
            return false;
        }
        if (i < p && a[i] == a[p]) {
            return false;
        }
    }
    return true;
}

static void check_case(const int a[], size_t n, size_t expected) {
    size_t actual = 0;
    assert(max_index(a, n, &actual));
    assert(actual == expected);
    assert(is_first_maximum(a, n, actual));
}

int main(void) {
    const int singleton[] = {7};
    const int duplicates[] = {4, 9, 3, 9, 7};
    const int descending[] = {8, 6, 4, 2};
    const int negatives[] = {-8, -2, -11};

    check_case(singleton, 1, 0);
    check_case(duplicates, 5, 1);
    check_case(descending, 4, 0);
    check_case(negatives, 3, 1);

    size_t ignored = 0;
    assert(!max_index(NULL, 0, &ignored));
    assert(!max_index(singleton, 1, NULL));

    puts("all correctness checks passed");
    return 0;
}

Compile with a strict C17 configuration and sanitizers during development:

cc -std=c17 -Wall -Wextra -Wpedantic -Wconversion \
   -fsanitize=address,undefined correctness.c -o correctness

The expected output is:

all correctness checks passed

Correctness Review

• A problem specification defines valid inputs and acceptable outputs independently of an implementation.
• Preconditions state the assumptions; postconditions state the promise.
• Partial correctness proves that any returned result is right. Total correctness also proves termination.
• A loop invariant must hold initially, survive every iteration, and imply the postcondition when the loop ends.
• Recursive correctness is normally strong induction plus a strictly decreasing measure.
• Direct proof, induction, and contradiction are reusable proof structures; a single valid counterexample refutes a universal claim.
• Tests reveal implementation defects and provide evidence, but finite testing cannot prove an unrestricted universal claim.
• Correctness depends on the model: overflow, invalid inputs, representation, aliasing, and tie behavior must not remain invisible assumptions.

Correctness Problems

Contract Language

1. State the difference between a problem, an instance, and an algorithm.
2. Distinguish a precondition from a postcondition using binary search as an example.
3. Explain why partial correctness does not exclude an infinite loop.
4. What three obligations form a loop-invariant proof?

Invariant Traces

5. Trace max_index on [5, 5, 4, 5]. Repeat after changing > to >=. State the postcondition satisfied by each version.
6. Trace gcd(544, 119). List the decreasing variant at every call.
7. For while (x > 1) x /= 2;, propose an invariant and a termination measure. How many iterations occur for x = 100?

Proof Construction

8. Prove that a loop summing a[0] through a[n-1] returns the mathematical sum. State an invariant strong enough to handle the empty array.
9. Prove by induction that recursive binary exponentiation computes x^n for every integer n >= 0.
10. Prove by contradiction that a finite undirected tree has at least two leaves when it has at least two vertices.

Breaking the Claim

11. This loop intends to compute the first index whose value is at least target in a sorted array:

    while (lo < hi) {
        size_t mid = lo + (hi - lo) / 2;
        if (a[mid] < target) {
            lo = mid;
        } else {
            hi = mid;
        }
    }

    Find a smallest input on which progress stops. Repair the update and state the decreasing variant.

12. A sorting test checks only that output is nondecreasing. Give two incorrect “sorting” functions that always pass that check, then add the missing property to the oracle.

Contract Design

13. Specify an algorithm that returns the second-largest distinct value. Decide what happens when fewer than two distinct values exist; state a loop invariant before writing code.
14. Specify a topological-sort interface. Your postcondition must cover both successful DAG input and cyclic input, without demanding one fixed valid order.
15. Design a property-based test for a function that reverses an array in place. Identify one property that is necessary but insufficient, then give a sufficient pair of properties.

Proof Challenges

16. The extended Euclidean algorithm returns integers x, y, and d satisfying ax + by = d = gcd(a,b). Derive a recursive invariant that proves the identity survives each return step.
17. Give a total-correctness proof for the two-pointer partition procedure used in quicksort. Be explicit about duplicate values and about the variant that forces the pointers to meet.