1
The two are independent
An algorithm can be partially correct and never stop, or terminate promptly with a wrong answer. Neither proof implies the other.
Lesson · Algorithms and Complexity · Foundations
Correctness and Termination
Partial correctness says the output is right if the algorithm stops. Termination says it stops. Loop invariants establish the first and a decreasing bounded quantity establishes the second.
PARTIAL CORRECTNESS if it terminates, the postcondition holds
TERMINATION it does terminate
TOTAL CORRECTNESS both
invariant for the first, a decreasing measure for the second
Two obligations
Core ideas
What this lesson establishes
This is “Loop Invariants and Program Correctness” in Induction and Recursion applied to algorithms, and the split is what makes the proofs short.
2
An invariant is what the loop preserves
Naming the preserved property is more informative than describing what the loop does, and it is what closes the argument.
3
Termination needs a decreasing measure
A quantity that strictly decreases on every iteration and cannot decrease forever. Usually an index or a remaining size.
The material
Proving an algorithm right
The two obligations, both discharged on three algorithms.
Definition · Partial and total correctness
An algorithm is partially correct when, if it terminates, its output satisfies the specification. It is totally correct when it is partially correct and terminates on every valid input.
Linear search
LINEAR-SEARCH(a, x):
for i = 1 to n:
if aᵢ = x: return i
return 0
INVARIANT before iteration i, x ∉ {a₁, …, a_{i−1}}
Initialisation. Before the first iteration the set is empty and the claim is vacuous. Maintenance. The iteration returns if aᵢ = x, so reaching the next iteration means x ≠ aᵢ, extending the invariant. Termination. If the loop finishes, the invariant says x is in none of a₁ … aₙ, so returning 0 is correct; if it returns i, then aᵢ = x.
Termination holds because n − i strictly decreases and is a non-negative integer.
Insertion sort
The outer-loop invariant is that a[1..j−1] holds the original first j−1 elements in sorted order. Both halves are needed: "sorted" alone would be satisfied by an algorithm that replaced the array with zeros, and the specification says the output must be a permutation of the input.
Termination: the outer loop runs n − 1 times, and the inner loop decreases i each iteration with i ≥ 0 enforced by its own condition.
Euclid's algorithm
The invariant is gcd(a, b) = gcd(a₀, b₀), preserved because gcd(a,b) = gcd(b, a mod b). Termination holds because b strictly decreases and is a non-negative integer. At exit b = 0 and gcd(a, 0) = a, which the invariant identifies as the answer.
That invariant is the whole proof and it is one line, which is characteristic: a good invariant names the quantity the loop preserves, and the correctness then follows from the exit condition.
When termination is the hard part
Example · The Collatz procedure
From n, repeat: if n is even, halve it; otherwise replace it by 3n + 1; stop at 1. It terminates for every starting value ever tested — beyond 10²⁰ — and no proof is known that it always does. Partial correctness is trivial; termination is an open problem.
That example separates the two obligations cleanly. It also previews “Decidability and the Halting Problem”: there is no general procedure that decides termination for arbitrary programs, which is why each one needs its own argument.
Interactive
Algorithms and growth
Counts from running, not from quoting
Method
Proving an algorithm correct
Invariant, then measure.
1
Write the specification
Precondition and postcondition. Without them there is nothing to prove.
2
Find an invariant strong enough
Test it at exit first: the invariant plus the negated loop condition must give the postcondition. If it does not, strengthen it.
3
Prove initialisation and maintenance
True before the first iteration, preserved by the body. This is base case and inductive step.
4
Exhibit a decreasing bounded measure
For termination. An index, a range size, a remaining count — strictly decreasing and bounded below.
Correctness
Score 0 / 0Choose the answer you can justify.
Exponentiation by squaring, both obligations
Number Theory and Cryptography's algorithm, proved.
POWER(x, n):
result = 1; base = x; m = n
while m > 0:
if m is odd: result = result · base
base = base · base
m = m div 2
return result
INVARIANT result · base^m = xⁿ
INITIALISATION 1 · x^n = xⁿ ✓
MAINTENANCE m even: result·(base²)^{m/2} = result·base^m ✓
m odd: (result·base)·(base²)^{(m−1)/2}
= result·base^m ✓
TERMINATION m halves each iteration, bounded below by 0 ✓
at exit m = 0, so invariant reads result = xⁿ ✓
The invariant was chosen to be exactly what the exit condition needs. That is the technique: work backwards from the postcondition, substitute the loop variable for its final value, and the invariant usually appears.
Common mistakes
1
Proving one obligation and stoppingBoth are required, and neither implies the other. Say explicitly which you have established.
2
Choosing an invariant that is too weak"The array is sorted" without "and is a permutation of the input" is satisfied by an algorithm that destroys the data.
3
Assuming loops obviously terminateName the decreasing quantity and its lower bound. It is one sentence and it is where an off-by-one shows.
Check your understanding
✓
Finish when you test the invariant at exit first.
Write a loop computing the sum of an array, state its invariant, and check that the invariant plus the exit condition gives exactly "the sum of all n elements". If it needs an extra sentence, strengthen the invariant.
Note: Hoare logic formalises this with a rule for each language construct, and modern verification tools mechanise it. What does not mechanise is finding the invariant, which remains the creative step.