The Central Idea
A correctness proof answers the question:
Why does this algorithm always produce the required answer when its stated assumptions are satisfied?
Testing can reveal errors, but testing finitely many examples cannot by itself prove correctness for every valid input.
Specifications
Before proving an algorithm correct, state what the algorithm is supposed to do.
A specification describes:
- the valid inputs;
- the required output;
- the relationship the output must have to the input.
A proof can only be as precise as the specification it is proving.
Preconditions
A precondition is an assumption that must be true before the algorithm begins.
For binary search, a central precondition is:
The input sequence is sorted according to the comparison rule.
Without that assumption, binary search is not guaranteed to be correct.
Postconditions
A postcondition is a condition that must be true when the algorithm finishes.
For a sorting algorithm, a suitable postcondition includes:
- the output sequence is ordered;
- the output contains exactly the same multiset of elements as the input.
Correctness Connects Preconditions to Postconditions
A correctness claim has the general form:
\[ \boxed{\text{If the preconditions hold, then after execution the postconditions hold.}} \]The proof explains why every permitted execution preserves the required logical relationship.
Partial Correctness
An algorithm is partially correct if:
Whenever it terminates on a valid input, its output satisfies the specification.
Partial correctness does not yet prove that the algorithm actually stops.
Total Correctness
An algorithm is totally correct if:
- it is partially correct;
- it terminates on every valid input.
Thus total correctness combines
\[ \boxed{\text{correct result}+\text{guaranteed termination}}. \]Termination will receive a dedicated treatment in the next lesson.
Why Examples Are Not Proofs
Suppose an algorithm gives the correct answer for \(1000\) test cases.
That evidence is valuable, but an untested input may still expose a defect.
A correctness proof must account for the structure of all valid inputs, not merely a sample.
Counterexamples
A single valid input on which an algorithm returns an incorrect answer is enough to disprove a universal correctness claim.
Such an input is a counterexample.
Therefore, correctness analysis often has two complementary activities:
- prove the algorithm when the claim is true;
- search for a counterexample when the claim is doubtful.
Loop Invariants
A loop invariant is a statement that remains true at a designated point in every loop iteration.
Invariants connect local steps of an iterative algorithm to its final correctness.
The Three Parts of an Invariant Proof
A standard loop-invariant proof has three parts:
- Initialization: prove the invariant before the first iteration.
- Maintenance: assuming it holds before one iteration, prove it still holds afterward.
- Use at termination: combine the invariant with the stopping condition to derive the postcondition.
Invariant Example: Linear Search
Suppose linear search examines positions from left to right.
A useful invariant is:
Before examining position \(i\), the target does not occur in any earlier position \(1,\ldots,i-1\).
This captures what has already been ruled out.
Initialization for Linear Search
Before the first position is examined, there are no earlier positions.
Therefore, the statement
The target does not occur in any earlier examined position
is vacuously true.
Maintenance for Linear Search
Assume the invariant holds before position \(i\) is examined.
If position \(i\) does not contain the target, then after advancing to \(i+1\), the target has been ruled out from positions
\[ 1,\ldots,i. \]Therefore, the invariant is preserved.
Using the Invariant at Termination
If linear search reaches the end without finding the target, then every position has been ruled out.
Therefore, the algorithm can correctly report
\[ \boxed{\text{target absent}}. \]Invariant Example: Selection Sort
A useful selection-sort invariant is:
At the start of each pass, the prefix already completed contains the smallest elements of the original input in sorted order.
The next pass extends this sorted prefix by one position.
Why the Selection-Sort Invariant Is Maintained
During each pass, the algorithm finds the smallest element in the remaining unsorted suffix.
Placing that element at the boundary ensures that the enlarged prefix still consists of the smallest elements in sorted order.
Invariant Example: Insertion Sort
A standard insertion-sort invariant is:
Before processing position \(i\), the prefix \(1,\ldots,i-1\) is sorted and contains exactly the elements originally in that prefix.
Inserting the next item in the correct position preserves both order and element preservation.
Invariants Need to Be Strong Enough
The statement
"Some part of the array is sorted"
may be true but too vague to prove correctness.
A useful invariant must contain enough information to connect the current state to the final postcondition.
Invariants Need to Be True
An invariant cannot be chosen merely because it would be convenient.
It must actually hold:
- before the first iteration;
- after every iteration in which the loop continues.
A false invariant cannot support a proof.
Assertions
An assertion is a logical statement about the current program state at a particular point.
Preconditions, postconditions, and invariants are all forms of assertions.
Correctness proofs reason about how algorithmic steps transform one true assertion into another.
Sequential Reasoning
Suppose an algorithm performs step \(A\) followed by step \(B\).
To prove the sequence correct, one may show:
- the precondition guarantees the assumptions needed for \(A\);
- after \(A\), an intermediate assertion holds;
- that assertion is sufficient for \(B\);
- after \(B\), the postcondition holds.
Conditional Correctness
For an if–else statement, the proof must consider each possible branch.
If the condition is true, prove the true branch leads to the postcondition.
If the condition is false, prove the false branch leads to the postcondition.
All permitted control-flow paths must be covered.
Recursive Correctness
Recursive algorithms are often proved correct using induction.
The structure is:
- prove the base case;
- assume recursive calls correctly solve smaller valid instances;
- show the current call uses those correct smaller answers to produce the correct larger answer.
Factorial Correctness
Consider the recursive rule
\[ F(0)=1 \]and
\[ F(n)=nF(n-1) \]for \(n\ge1\).
We want to prove
\[ F(n)=n!. \]Base Case for Factorial
At \(n=0\),
\[ F(0)=1. \]By definition,
\[ 0!=1. \]Therefore, the claim holds for the base case.
Inductive Step for Factorial
Assume
\[ F(n-1)=(n-1)!. \]Then
\[ F(n)=nF(n-1) \] \[ =n(n-1)! \] \[ =\boxed{n!}. \]Thus the recursive computation is correct for \(n\) if it is correct for \(n-1\).
Strong Induction in Algorithm Proofs
Some algorithms depend on several smaller subproblems.
In such cases, strong induction is often natural.
Assume correctness for all smaller input sizes
\[ 0,1,\ldots,n-1 \]and use those assumptions to prove correctness for size \(n\).
Divide-and-Conquer Correctness
A divide-and-conquer proof usually separates:
- correctness of the base cases;
- correctness of the recursive subproblem solutions;
- correctness of the combine step.
The combine step must transform correct subproblem answers into a correct answer for the full problem.
Merge Sort Correctness
Merge sort relies on two claims:
- the recursive calls correctly sort the two halves;
- the merge procedure correctly combines two sorted lists into one sorted list containing all original elements.
Proving both establishes the overall result.
Correctness of Binary Search
Binary search relies on the invariant:
If the target is present, it lies within the current search interval.
Because the data is sorted, comparing the target with the middle entry allows one half to be removed without discarding a possible target.
Binary Search Maintenance
Suppose the target is smaller than the middle entry.
Because the list is sorted, every element to the right is at least as large as the middle entry.
Therefore, the target cannot be in that right region.
Keeping only the left half preserves the invariant.
Graph-Algorithm Correctness
Graph proofs often depend on structural invariants.
Examples include:
- BFS processes vertices by increasing distance layer;
- Kruskal's selected edges remain acyclic;
- Prim's selected edges remain connected;
- Dijkstra settles only vertices whose shortest distance is final under nonnegative weights.
Greedy Correctness
Greedy algorithms require more than showing that each chosen step looks locally good.
A proof must show that the greedy choice is compatible with some global optimum.
Common techniques include:
- exchange arguments;
- staying-ahead arguments;
- cut-and-paste reasoning.
Dynamic-Programming Correctness
A dynamic-programming proof typically verifies:
- the state meaning is correct;
- the base states are correct;
- the recurrence includes every valid way to build the state;
- the recurrence combines or optimizes those possibilities correctly.
Backtracking Correctness
A backtracking proof must show:
- every reported complete candidate is valid;
- every valid candidate is explored unless safely pruned;
- every pruning rule removes only branches that cannot contain a required solution.
Soundness
An algorithm is sound if every answer it reports as valid really is valid.
In a search problem:
\[ \boxed{\text{reported solution}\implies\text{actual solution}}. \]Soundness prevents false positives.
Completeness
An algorithm is complete if it does not miss required solutions.
In an existence search:
\[ \boxed{\text{solution exists}\implies\text{algorithm can find one}}. \]Completeness prevents false negatives.
Soundness and Completeness Together
For many decision and search algorithms, correctness can be organized into two directions:
- if the algorithm says yes, justify why yes is true;
- if the correct answer is yes, justify why the algorithm will not miss it.
This is often clearer than one long proof.
Preservation of Data
Some algorithms transform data rather than decide a yes-or-no question.
Then correctness may require proving that important information is preserved.
For sorting:
\[ \boxed{\text{output is a permutation of input}}. \]Order alone is not enough.
Safety Properties
A safety property says that something bad never happens.
Examples include:
- a spanning-tree algorithm never introduces a cycle;
- an array index never leaves its valid range;
- a partial coloring never assigns the same color to adjacent vertices.
Progress Properties
A progress property says that the algorithm continues moving toward completion or toward a required result.
Progress is especially important for total correctness.
In the next lesson, termination arguments will formalize this idea.
Edge Cases
Correctness proofs must cover valid boundary inputs.
Typical edge cases include:
- empty inputs;
- one-element inputs;
- duplicate values;
- already sorted data;
- disconnected graphs;
- minimum or maximum allowed parameter values.
Why Edge Cases Matter
An algorithm can behave correctly on large ordinary inputs but fail on the smallest valid case.
Base cases and loop boundaries are frequent sources of such errors.
A proof should explicitly account for them.
Off-by-One Errors
An off-by-one error occurs when a loop or index range includes one position too many or one too few.
Correctness reasoning can expose such errors by asking exactly which positions have been processed at each stage.
Specifications Must Match the Intended Problem
An algorithm may be perfectly correct for the wrong specification.
For example, an algorithm that finds a minimum-edge path is not necessarily solving a minimum-weight path problem.
The proof must justify the intended objective, not a nearby one.
Algorithm Assumptions Are Part of the Proof
Dijkstra's algorithm assumes nonnegative edge weights.
Binary search assumes sorted data.
A topological sort assumes acyclicity if it is expected to return an ordering.
Ignoring such assumptions invalidates the correctness claim.
Common Error: Proving the Intended Algorithm Instead of the Written One
A proof must match the actual procedure.
If the code updates the wrong index, uses the wrong comparison, or skips a case, proving a corrected version does not prove the given algorithm.
Always align the proof with the exact steps being executed.
Common Error: Circular Reasoning
A correctness proof cannot assume the final result in order to justify an intermediate step.
The reasoning should proceed from established assumptions, invariants, and previously proved facts.
Common Error: Weak Invariant
An invariant may be true throughout the algorithm but still fail to imply the postcondition at termination.
Such an invariant is too weak for the proof.
Strengthen it until it records enough information about the processed region.
Common Error: Forgetting Initialization
Proving that a loop preserves an invariant is not enough.
The invariant must also be true before the first iteration.
Common Error: Forgetting the Termination Connection
An invariant can hold forever without proving the desired result.
The proof must explain why
\[ \text{invariant}+\text{loop exit condition} \]implies the required postcondition.
Common Error: Assuming Termination While Claiming Total Correctness
Partial correctness alone does not prove total correctness.
A separate termination argument is required.
This distinction is essential for recursive algorithms and loops whose progress is not immediately obvious.
Common Error: Relying Only on Testing
Testing is valuable for finding bugs and validating implementation details.
But a finite test suite does not establish a universal mathematical guarantee.
Correctness proofs and tests serve different purposes.
A Reliable Procedure for Proving Algorithm Correctness
- State the valid input domain.
- State the required postcondition precisely.
- List any assumptions or preconditions.
- Identify the major control structure: sequence, branch, loop, recursion, greedy step, dynamic-programming recurrence, or search tree.
- Choose an appropriate invariant or inductive claim.
- Prove initialization or the base case.
- Prove maintenance or the inductive step.
- Show how the final state implies the postcondition.
- Check edge cases and hidden assumptions.
- Prove termination separately when total correctness is required.
Example: Maximum of a List
Consider an algorithm that scans a nonempty list and stores a variable \(m\), initially equal to the first entry.
Whenever a later entry is larger than \(m\), replace \(m\) with that entry.
A useful invariant is:
After processing the first \(i\) entries, \(m\) equals the maximum of those \(i\) entries.
Maximum Algorithm: Initialization
After processing only the first entry,
\[ m=a_1. \]The maximum of the one-element prefix is \(a_1\), so the invariant holds.
Maximum Algorithm: Maintenance
Assume \(m\) is the maximum of the first \(i\) entries.
When entry \(a_{i+1}\) is processed, the new maximum is
\[ \max\{m,a_{i+1}\}. \]The update rule assigns exactly this value to \(m\).
Therefore, the invariant is preserved.
Maximum Algorithm: Conclusion
When the scan ends, all \(n\) entries have been processed.
By the invariant,
\[ m=\max\{a_1,\ldots,a_n\}. \]Therefore, the algorithm returns the correct maximum.
Example: Correctness of a Simple Sum
Suppose an algorithm initializes
\[ s=0 \]and then adds each list entry to \(s\).
A useful invariant is:
\[ \boxed{s=a_1+a_2+\cdots+a_i} \]after the first \(i\) entries have been processed.
Practice 1: Preconditions
What important precondition is required for ordinary binary search?
Practice 2: Postcondition
Give two properties that should appear in the postcondition of a sorting algorithm.
Practice 3: Partial Correctness
What does partial correctness guarantee?
Practice 4: Total Correctness
What additional requirement turns partial correctness into total correctness?
Practice 5: Loop Invariant
An algorithm scans a list while maintaining a variable \(m\).
State a useful invariant for proving that \(m\) becomes the list maximum.
Practice 6: Invariant Proof Structure
Name the three standard parts of a loop-invariant proof.
Practice 7: Recursive Correctness
What proof technique is naturally associated with recursive algorithms?
Practice 8: Soundness
In a search problem, what does soundness prevent?
Practice 9: Counterexample
How many valid counterexamples are needed to disprove a claim that an algorithm is correct for every valid input?
Practice 10: Weak Invariant
Why is a true but very weak invariant sometimes insufficient for a correctness proof?
Practice Answers
Practice 1
The input must be
\[ \boxed{\text{sorted according to the comparison rule}}. \]Practice 2
A correct sorting postcondition should state that:
- the output is in the required order;
- the output contains exactly the same multiset of elements as the input.
Practice 3
Partial correctness guarantees that
\[ \boxed{\text{if the algorithm terminates, its output is correct}}. \]Practice 4
We must also prove
\[ \boxed{\text{termination on every valid input}}. \]Practice 5
A useful invariant is:
After processing the first \(i\) entries, \(m\) equals the maximum of those \(i\) entries.
Practice 6
The three parts are:
\[ \boxed{\text{initialization, maintenance, use at termination}}. \]Practice 7
Recursive correctness is naturally proved using
\[ \boxed{\text{mathematical induction}} \]or strong induction when several smaller subproblems are involved.
Practice 8
Soundness prevents
\[ \boxed{\text{false positives}}. \]Practice 9
Only
\[ \boxed{1} \]valid counterexample is needed.
Practice 10
The invariant may fail to contain enough information to imply the required postcondition when the algorithm stops.
What to Remember
- Correctness begins with a precise specification.
- Preconditions describe assumptions on valid inputs.
- Postconditions describe what must be true after successful execution.
- Partial correctness proves the answer is right if the algorithm terminates.
- Total correctness adds guaranteed termination.
- Loop invariants are proved through initialization, maintenance, and use at termination.
- Recursive correctness often mirrors induction.
- Soundness prevents false positives; completeness prevents missed valid solutions.
- One counterexample is enough to refute a universal correctness claim.
- Algorithm assumptions must be included in the correctness claim.
The most important habit is: state exactly what must be true before, during, and after the algorithm—and prove the algorithm preserves that logic.
Where We Go Next
A correctness proof can show that an algorithm returns the right answer if it finishes. To establish total correctness, we must also prove that the procedure cannot continue forever.
The next lesson, Termination, develops progress measures, variants, well-founded descent, recursive termination, loop termination, and common sources of nontermination.