Introduction to Algorithms

Algorithm Correctness

A Comprehensive Guide with Examples and

Proofs

Author: Your Name

February 18, 2026

“A correct algorithm is not accidental. It is proven.”

Contents

1
Preface
This document is a thorough exploration of algorithm correctness. We be-
gin with the fundamental question: what does it mean for an algorithm to
be correct? We then dissect correctness into partial correctness and termi-
nation, and combine them into total correctness. Through numerous exam-
ples, we demonstrate how to prove algorithms correct using preconditions,
postconditions, and loop invariants. Special attention is given to loops—
the heart of most algorithms—and a five-point checklist ensures that no
detail is overlooked. By the end, you will be equipped to reason about the
correctness of any algorithm you design or encounter.

2
 1 Why Algorithm Correctness Matters
In the early days of computing, programs were small and correctness could
often be verified by inspection. Today, software systems consist of millions
of lines of code, and even a single logical error can lead to catastrophic
failures. Consider the following historical incidents:

• Therac-25 (1985–1987): A radiation therapy machine caused patient

deaths due to a race condition and inadequate software testing.

• Ariane 5 Flight 501 (1996): A software exception caused by an inte-

ger overflow led to the rocket’s self-destruction.

• Intel Pentium FDIV Bug (1994): A flaw in the floating-point division

algorithm caused incorrect results for certain inputs.

• Knight Capital Group (2012): A software glitch caused a 440millionlossin45minutes.

These incidents underscore that an algorithm is valuable not because it
runs, but because it produces the right result for the right input under the
right conditions. Algorithm correctness is the discipline that allows us to
answer the question:

“Does this algorithm always do what it claims to do?”

Important Insight
Correctness is about truth, not appearance. An algorithm that com-
piles and runs without crashing may still be utterly wrong.

2 What Does It Mean for an Algorithm to Be Cor-

rect?
Correctness is not a single property; it comprises two essential components:

1. Partial Correctness: If the algorithm terminates, the result is correct.

2. Termination: The algorithm always stops after a finite number of

steps.

3
 When both are satisfied, we say the algorithm is totally correct.
Key Definition
An algorithm is totally correct if it is partially correct and guaranteed
to terminate.

2.1 Partial Correctness Illustrated

Start

Algorithm Runs

Algorithm Stops

Output is Correct

Partial correctness only cares about the path that leads to termination.
If the algorithm never stops, partial correctness makes no claim.

2.2 Termination Illustrated

Start

Algorithm Runs Runs Forever

Algorithm Stops

4
 Termination requires that the path to ”Runs Forever” does not exist.

2.3 Examples of Partial vs. Total Correctness

Example
Partial Correctness but Non-Termination:
1 def find_first_zero (A):
2 i = 0
3 while True : # infinite loop
4 if A[i] == 0:
5 return i
6 i = i + 1
If the loop were to terminate (e.g., by an external interrupt), it would
return the correct index of the first zero. Hence it is partially correct,
but not totally correct because it may never terminate (if no zero ex-
ists).

Example
Termination but Incorrect Output:
1 def average (A):
2 sum = 0
3 for i in range (len(A)):
4 sum = sum + A[i]
5 return sum // len(A) # integer division
This algorithm always terminates, but if the true average is fractional,
it returns a truncated (incorrect) value. It is terminating but not par-
tially correct (with respect to real-number average).

5
 Example
Totally Correct:
1 def max_element (A):
2 if len(A) == 0:
3 return None # handle empty case
4 max_val = A [0]
5 for i in range (1 , len(A)):
6 if A[i] > max_val :
7 max_val = A[i]
8 return max_val
Termination is guaranteed by the finite loop, and the result is always
the maximum. This algorithm is totally correct (assuming we define
the empty case appropriately).

3 Preconditions and Postconditions

To reason about correctness formally, we need precise statements about
what must be true before and after an algorithm runs.
Key Definition
A precondition is a condition that must be true before an algorithm
begins execution. A postcondition is a condition that must be true
after the algorithm terminates.

Preconditions and postconditions form a contract: if the caller ensures

the precondition, the algorithm guarantees the postcondition.

6
 Example
Binary Search Pre/Post:

• Precondition: The input array A[0..n − 1] is sorted in non-

decreasing order.

• Postcondition: Returns an index i such that A[i] = x, or −1 if x

is not present.

If the caller provides an unsorted array, the algorithm may behave in-
correctly (the contract is broken).

3.1 Why Preconditions Matter

Preconditions protect the algorithm from invalid inputs. For example, an
algorithm that computes the square root of a number might have the pre-
condition x ≥ 0. If called with a negative number, the behavior is unde-
fined (or an exception is raised). By documenting preconditions, we make
the algorithm’s assumptions explicit.

3.2 Postconditions as Guarantees

Postconditions tell the caller what to expect. They must be strong enough
to be useful but weak enough to be achievable. For instance, a sorting algo-
rithm’s postcondition might be: ”The output array is a permutation of the
input and is sorted in non-decreasing order.”

4 Loop Invariants: The Key to Proving Correct-

ness
Loops are the heart of most algorithms. They allow repetition, but they
also introduce complexity in correctness proofs. A loop that is not carefully
designed can easily be incorrect or non-terminating.

7
 Key Definition
A loop invariant is a condition that is true before the loop starts, re-
mains true after each iteration, and helps prove correctness at termi-
nation.

To prove a loop correct, we establish three properties:

1. Initialization: The invariant holds before the first iteration.

2. Maintenance: If the invariant holds before an iteration, it holds after

the iteration.

3. Termination: The loop will eventually stop, and at that point the in-
variant (plus the loop condition false) implies the desired postcondi-
tion.

These three steps together guarantee total correctness (provided the

loop body itself is correct).

4.1 Illustrating a Loop Invariant

Invariant true
before loop
iteration 1
Invariant true
after iteration 1
iteration 2
Invariant true
after iteration
... 2
Invariant true
after final iteration
+ loop condition false
⇒ postcondition

8
4.2 Example 1: Finding the Maximum Element
Example
Problem: Given a non-empty array A[0..n − 1], find the maximum
element.
Precondition: n ≥ 1.
Postcondition: Returns max such that max is the largest value in A.
Pseudocode:
1 def max_element (A):
2 max_val = A [0]
3 i = 1
4 while i < len(A):
5 if A[i] > max_val :
6 max_val = A[i]
7 i = i + 1
8 return max_val

4.2.1 Loop Invariant

At the beginning of each iteration (just before the condition check), the
variable max_val holds the maximum of the subarray A[0..i − 1].

9
4.2.2 Proof of Correctness
Proof
• Initialization: Before the loop, i = 1. The subarray A[0..0] con-
sists of the first element, and max_val = A[0], which is trivially
the maximum of that single element. Invariant holds.

• Maintenance: Assume invariant holds at the beginning of an it-

eration with current i (so max_val = max of A[0..i−1]). We com-
pare A[i] with max_val. If A[i] > max_val, we update max_val
to A[i]; otherwise max_val stays. After the update, max_val now
equals the maximum of A[0..i] because we have included A[i] in
the comparison. Then we increment i to i + 1. At the start of the
next loop body, i is now the new index, and max_val is the max-
imum of A[0..i − 1] (since i was incremented). Thus invariant
restored.

• Termination: The loop runs while i < n. Each iteration incre-

ments i by 1, so after at most n − 1 iterations, i becomes n, and
the loop condition fails. At that point, invariant says max_val
is the maximum of A[0..n − 1], which is the entire array. Hence
postcondition holds.

10
4.3 Example 2: Sum of Array Elements
Example
Problem: Given an array A[0..n − 1] (possibly empty), compute the
sum of its elements.
Precondition: None (empty array sum is 0).
∑
Postcondition: Returns sum = n−1
j=0 A[j].
Pseudocode:
1 def array_sum (A):
2 s = 0
3 i = 0
4 while i < len(A):
5 s = s + A[i]
6 i = i + 1
7 return s

4.3.1 Loop Invariant

At the beginning of each iteration, s equals the sum of the first i elements:
∑
s = i−1
j=0 A[j].

4.3.2 Proof of Correctness

Proof
• Initialization: Before the loop, i = 0, so s = 0 which is the sum
of zero elements (empty sum). Invariant holds.

• Maintenance: ∑ Assume invariant holds at start of iteration with

current i: s = i−1j=0 A[j]. We add A[i] to s, so after the addition,
∑i
s = j=0 A[j]. Then we increment i to i+1, so at the beginning of
∑
the next iteration, s equals i−1
j=0 A[j] (where i is the new index).
Invariant restored.

• Termination: The loop runs while i < n. Each iteration incre-

ments i, so after n iterations, i = n and loop exits. At that point,
∑
invariant says s = n−1 j=0 A[j], which is exactly the postcondition.

11
4.4 Example 3: Linear Search
Example
Problem: Given an array A[0..n − 1] and a target x, return the smallest
index i such that A[i] = x, or −1 if not found.
Precondition: None (array can be empty).
Postcondition: If x is in A, return i with A[i] = x and for all j < i,
A[j] ̸= x; otherwise return −1.
Pseudocode:
1 def linear_search (A, x):
2 i = 0
3 while i < len(A):
4 if A[i] == x:
5 return i
6 i = i + 1
7 return -1

4.4.1 Loop Invariant

At the beginning of each iteration, x is not present in A[0..i − 1].

12
4.4.2 Proof of Correctness
Proof
• Initialization: i = 0, so A[0..−1] is empty, trivially x not present.
Invariant holds.

• Maintenance: Assume invariant holds (no x in A[0..i − 1]). We

check A[i]. If A[i] == x, we return immediately and postcondi-
tion is satisfied (the returned i is correct, and because of invari-
ant, no earlier index contained x). If A[i] ̸= x, we increment i to
i + 1. Now the invariant for the next iteration (no x in A[0..i − 1])
holds because we just verified A[i] was not x and earlier indices
were already free of x.

• Termination: The loop variable i increases each step; either we

find x and return (terminating early), or i reaches n and loop
ends. In the latter case, invariant plus loop condition false (i =
n) tells us x is not in A[0..n − 1], i.e., not in the whole array, so
we return −1 correctly.

4.5 Example 4: Binary Search

Binary search is a classic example where a clear loop invariant is essential.

13
 Example
Problem: Given a sorted array A[0..n − 1] (ascending) and a target x,
return any index where x appears, or −1 if absent.
Precondition: A is sorted in non-decreasing order.
Postcondition: If x is in A, return an index i with A[i] = x; otherwise
return −1.
Pseudocode (typical implementation):
1 def binary_search (A, x):
2 low = 0
3 high = len(A) - 1
4 while low <= high :
5 mid = ( low + high ) // 2
6 if A[ mid ] == x:
7 return mid
8 elif A[ mid ] < x:
9 low = mid + 1
10 else :
11 high = mid - 1
12 return -1

4.5.1 Loop Invariant

At the beginning of each iteration, if x is in the array, then it must lie in the
subarray A[low..high] (inclusive). In other words, the target, if present, is
confined to the current search interval.

14
4.5.2 Proof of Correctness
Proof
• Initialization: Initially low = 0, high = n − 1, so the interval is
the whole array. If x is present, it is certainly in [0, n − 1]. Invari-
ant holds.

• Maintenance: Suppose invariant holds and low ≤ high. Com-

pute mid.

– If A[mid] == x, we return immediately (correct).

– If A[mid] < x, then because the array is sorted, all ele-
ments at indices ≤ mid are ≤ A[mid] < x, so x cannot be
in [low, mid]. Thus if x exists, it must be in [mid + 1, high].
Setting low = mid + 1 preserves the invariant.
– If A[mid] > x, then x cannot be in [mid, high], so set high =
mid − 1. Invariant preserved.

• Termination: Each iteration either returns (terminates) or re-

duces the size of the interval (high − low + 1) because either
low increases or high decreases. Since the interval size is a
non-negative integer, it cannot decrease indefinitely. Eventually
low > high, loop condition fails. At that point, invariant says if
x were present, it would have to be in [low, high] which is empty.
Hence x is not present, and we return −1 correctly.

5 Five Key Points for Testing Loops

When designing or reviewing loop-based algorithms, always verify these
five aspects:

15
 Checklist
1. Initialization: Does the loop start with correct state? (e.g., vari-
ables set correctly before first iteration)

2. Maintenance: Does each iteration preserve the loop invariant?

(i.e., if the invariant holds before an iteration, does it hold after?)

3. Termination: Will the loop definitely stop? Identify a loop vari-

ant (a metric that decreases/increases and has a bound) to prove
termination.

4. Coverage: Does the loop handle all cases, including edge cases?
(e.g., empty input, single element, duplicates, extreme values)

5. Postcondition: At loop exit, does the invariant plus the loop con-
dition false guarantee the desired result?

These five points form a robust checklist for loop correctness.

5.1 Detailed Examination of Each Point

5.1.1 1. Initialization
The invariant must be true just before the loop begins. This often involves
setting loop variables to initial values that satisfy the invariant. For exam-
ple, in the maximum algorithm, we set max_val = A[0] and i = 1; the
invariant ”max_val is the maximum of A[0..i − 1]” holds because A[0..0] is
just {A[0]}.

5.1.2 2. Maintenance
We must show that if the invariant holds at the start of an iteration, after
executing the loop body (and updating the loop variable), the invariant
holds again for the next iteration. This typically involves reasoning about
how the loop body changes the state.

16
5.1.3 3. Termination
We need a measure that strictly decreases (or increases) with each iteration
and cannot go beyond a bound. Common measures:

• Loop counter i increasing to n (as in for-loops). size in binary search.

• Value of a variable that is guaranteed to approach a limit.

If no such measure exists, the loop may run forever.

5.1.4 4. Coverage
Edge cases must be considered:

• Empty input: Does the loop handle it? (e.g., while loop condition
false immediately)

• Single element: Does the loop produce correct result?

• Duplicates: Does the algorithm behave as expected?

• Extreme values: Large numbers, negative numbers, etc.

Testing coverage helps catch off-by-one errors and other boundary issues.

5.1.5 5. Postcondition
At loop exit, the loop condition is false, and the invariant still holds. To-
gether, they should imply the desired postcondition. For example, in the
∑
sum algorithm, exit condition i = n and invariant s = i−1 j=0 A[j] together
∑n−1
give s = j=0 A[j], which is the postcondition.

17
6 More Examples with Loop Invariants
6.1 Example 5: Factorial
Example
Problem: Compute n! for n ≥ 0.
Precondition: n ≥ 0.
Postcondition: Returns n! = 1 × 2 × · · · × n (with 0! = 1).
Pseudocode:
1 def factorial (n):
2 result = 1
3 i = 1
4 while i <= n:
5 result = result * i
6 i = i + 1
7 return result

6.1.1 Loop Invariant

At the beginning of each iteration, result = (i − 1)! and i ≤ n + 1 (or more
precisely, after k iterations, result = k! and i = k + 1). A clean invariant:
result = (i − 1)!.

6.1.2 Proof
• Initialization: i = 1, so (i − 1)! = 0! = 1, and result = 1. Invariant
holds.

• Maintenance: Assume invariant holds at start: result = (i − 1)!. We

multiply result by i, obtaining result = (i−1)!×i = i!. Then we incre-
ment i to i + 1. Now at the beginning of the next iteration, result = i!
(with the old i) but i is now one larger, so result = ((inew − 1)!).
Invariant restored.

• Termination: The loop runs while i ≤ n. Each iteration increments i,

so after n iterations, i = n + 1, loop condition false. At exit, invariant
gives result = (i − 1)! = n!, which is the postcondition.

18
6.2 Example 6: Fibonacci Numbers
Example
Problem: Compute the n-th Fibonacci number Fn , where F0 = 0, F1 =
1, and Fn = Fn−1 + Fn−2 for n ≥ 2.
Precondition: n ≥ 0.
Postcondition: Returns Fn .
Pseudocode:
1 def fibonacci (n):
2 if n == 0:
3 return 0
4 elif n == 1:
5 return 1
6 a = 0 # F_{i -2}
7 b = 1 # F_{i -1}
8 i = 2
9 while i <= n:
10 c = a + b # F_i
11 a = b
12 b = c
13 i = i + 1
14 return b

6.2.1 Loop Invariant

At the beginning of each iteration (with current i), we have a = Fi−2 and
b = Fi−1 . (For i = 2, a = F0 = 0, b = F1 = 1.)

6.2.2 Proof
• Initialization: For i = 2, a = 0 = F0 , b = 1 = F1 . Invariant holds.

• Maintenance: Assume invariant holds at start: a = Fi−2 , b = Fi−1 .

Compute c = a + b = Fi−2 + Fi−1 = Fi . Then set a = b = Fi−1 ,
b = c = Fi . Increment i to i + 1. Now a = Fi−1 (since new i is old i + 1,
F(i+1)−2 = Fi−1 ) and b = Fi (since F(i+1)−1 = Fi ). Invariant holds for
the next iteration.

• Termination: Loop runs while i ≤ n. Each iteration increments i, so

after n − 1 steps (since we started at i = 2), i = n + 1 and loop exits.

19
 At exit, b = Fi−1 = Fn , satisfying postcondition.

6.3 Example 7: Array Reversal

Example
Problem: Reverse an array A[0..n − 1] in place.
Precondition: None.
Postcondition: The array is reversed: A[i] = original[n − 1 − i] for all
i.
Pseudocode:
1 def reverse_array (A):
2 i = 0
3 j = len(A) - 1
4 while i < j:
5 swap (A[i], A[j])
6 i = i + 1
7 j = j - 1

6.3.1 Loop Invariant

At the beginning of each iteration, the subarray A[0..i−1] has been reversed
with the subarray A[j + 1..n − 1]; more precisely, the elements outside the
current range [i, j] are already in their final reversed positions.

6.3.2 Proof
• Initialization: i = 0, j = n − 1, so the ranges A[0.. − 1] and A[n..n − 1]
are empty, trivially satisfied.

• Maintenance: Assume invariant holds. After swapping A[i] and A[j],

these two elements are placed correctly (since i should map to j and
vice versa). Then we increment i and decrement j, so the invariant
holds for the next iteration: the elements outside [i, j] (including the
ones just swapped) are in final positions.

• Termination: Loop runs while i < j. Each iteration brings i and j

closer together; eventually i ≥ j, loop condition false. At that point,

20
 if n is odd, the middle element is already in place; if even, all elements
have been swapped. The array is fully reversed.

6.4 Example 8: Selection Sort

Selection sort repeatedly finds the minimum element from the unsorted
part and places it at the beginning.
Example
Problem: Sort array A[0..n − 1] in non-decreasing order.
Precondition: None.
Postcondition: A is sorted.
Pseudocode:
1 def selection_sort (A):
2 n = len(A)
3 for i in range (n):
4 min_index = i
5 for j in range (i+1 , n):
6 if A[j] < A[ min_index ]:
7 min_index = j
8 swap (A[i], A[ min_index ])

We focus on the outer loop invariant.

6.4.1 Outer Loop Invariant

At the beginning of iteration i (for the outer loop), the subarray A[0..i − 1]
is sorted and contains the smallest i elements of the original array, in their
final positions.

6.4.2 Proof
• Initialization: i = 0, A[0.. − 1] empty, trivially sorted.

• Maintenance: Assume invariant holds for i. The inner loop finds the
index of the minimum element in A[i..n − 1]. Swapping it with A[i]
places that minimum at position i. Since A[0..i − 1] already contained
the smallest i elements, and the new element is the smallest among

21
 the remaining, after the swap, A[0..i] is sorted and contains the small-
est i + 1 elements. For the next iteration, i increments, so invariant
holds.

• Termination: The outer loop runs for i = 0 to n − 1, a finite number

of steps. At termination, i = n, so invariant says A[0..n − 1] is sorted,
which is the postcondition.

6.5 Example 9: Insertion Sort

Insertion sort builds the sorted array one element at a time by inserting
each new element into its correct position.
Example
Problem: Sort array A[0..n − 1].
Precondition: None.
Postcondition: A is sorted.
Pseudocode:
1 def insertion_sort (A):
2 for i in range (1 , len(A)):
3 key = A[i]
4 j = i - 1
5 while j >= 0 and A[j] > key :
6 A[j +1] = A[j]
7 j = j - 1
8 A[j +1] = key

6.5.1 Outer Loop Invariant

At the beginning of iteration i, the subarray A[0..i − 1] is sorted.

6.5.2 Proof
• Initialization: i = 1, A[0..0] is trivially sorted.

• Maintenance: Assume A[0..i − 1] is sorted. The inner while loop

shifts elements greater than key to the right, creating a hole where
key belongs. Inserting key into that hole yields a sorted A[0..i]. After
incrementing i, the invariant holds for the next iteration.

22
 • Termination: The outer loop runs n − 1 times, so it terminates. At
exit, i = n, so A[0..n − 1] is sorted.

7 Common Sources of Incorrect Algorithms

Even experienced programmers make mistakes. Recognizing common pit-
falls helps avoid them.

• Missing or incorrect preconditions: e.g., assuming array is sorted

for binary search but not checking or documenting it.

• Off-by-one errors: Loop boundaries, array indices. Example: using

‘while i <= n‘ when ‘i < n‘ is correct.

• Infinite loops: No progress toward termination, or loop condition

never becomes false. Example: forgetting to increment the loop vari-
able.

• Incorrect termination conditions: Stopping too early or too late. Ex-

ample: in binary search, using ‘low < high‘ instead of ‘low <= high‘.

• Assuming ideal input: Not handling edge cases like empty input,
duplicates, or negative numbers.

• Wrong loop invariant: Using an invariant that does not hold or does
not lead to the postcondition.

• Mutation of loop control variable inside: Accidentally modifying

the index variable in a way that breaks progress.

• Integer overflow: In languages without arbitrary-precision integers,

calculations may overflow, leading to incorrect results or undefined
behavior.

• Floating-point inaccuracies: Comparing floating-point numbers for

equality can be unreliable.

• Side effects: Modifying input data unintentionally.

23
 Example
Off-by-one error example:
1 def sum_first_n (n):
2 total = 0
3 i = 0
4 while i <= n: # should be i < n
5 total = total + i
6 i = i + 1
7 return total
This computes 0 + 1 + 2 + · · · + n instead of 0 + 1 + · · · + (n − 1).

Example
Infinite loop example:
1 def print_numbers (n):
2 i = 0
3 while i < n:
4 print (i)
5 # forgot to increment i
This will print 0 forever.

8 Formal Methods: Hoare Logic

For those interested in a more rigorous approach, Hoare logic provides a
formal system for reasoning about program correctness. It uses triples of
the form {P } C {Q}, where P is a precondition, C is a command, and Q
is a postcondition. The triple means: if P holds before executing C, and C
terminates, then Q holds afterwards.
Hoare logic includes axioms and rules for each programming construct:

• Assignment axiom: {Q[E/x]} x := E {Q}

• Composition rule: {P } C1 {R}, {R} C2 {Q} ⊢ {P } C1 ; C2 {Q}

• Conditional rule: {P ∧B} C1 {Q}, {P ∧¬B} C2 {Q} ⊢ {P } if B then C1 else C2 {Q

• While rule: {I ∧ B} C {I} ⊢ {I} while B do C {I ∧ ¬B}, where I is

the loop invariant.

24
 While Hoare logic is beyond the scope of this introductory document,
it underpins the loop invariant method we have been using.

9 Case Study: A Buggy Algorithm and Its Cor-

rection
Let’s examine a buggy implementation of binary search and see how the
loop invariant helps identify the error.
Example
Buggy Binary Search:
1 def buggy_binary_search (A, x):
2 low = 0
3 high = len(A) - 1
4 while low < high : # error : should be <=
5 mid = ( low + high ) // 2
6 if A[ mid ] == x:
7 return mid
8 elif A[ mid ] < x:
9 low = mid
10 else :
11 high = mid
12 return -1

9.0.1 What’s wrong?

1. The loop condition ‘low < high‘ means that when ‘low == high‘, the
loop exits without checking that element.

2. When updating, ‘low = mid‘ or ‘high = mid‘ can cause infinite loops
if ‘mid‘ doesn’t change (e.g., when ‘low‘ and ‘high‘ are adjacent).

Let’s test with an array of one element: A = [5], x = 5. Initially ‘low=0‘,

‘high=0‘. Loop condition ‘low < high‘ is false, so we skip the loop and
return -1. Incorrect.
Test with A = [1, 3], x = 2. - ‘low=0, high=1‘, condition true. ‘mid=0‘,
A[0] = 1 < 2, so ‘low=mid=0‘. Now ‘low=0, high=1‘ again, infinite loop.

25
 9.0.2 Corrected Version

1 def binary_search (A, x):

2 low = 0
3 high = len(A) - 1
4 while low <= high :
5 mid = ( low + high ) // 2
6 if A[ mid ] == x:
7 return mid
8 elif A[ mid ] < x:
9 low = mid + 1
10 else :
11 high = mid - 1
12 return -1

9.0.3 Invariant and Correctness

The invariant we used earlier holds, and termination is guaranteed because
each step reduces the interval size.

10 Exercises for the Reader

Test your understanding with these exercises.

1. Array Minimum: Write an algorithm to find the minimum element

in an array. State its precondition, postcondition, loop invariant, and
prove correctness.

2. Array Equality: Given two arrays A and B of the same length, de-
termine if they are equal element-wise. Provide a loop invariant and
prove correctness.

3. Power Function: Implement an algorithm to compute xn for integer

n ≥ 0 using a loop. Use a loop invariant to prove it correct.

4. Palindrome Check: Write an algorithm to check if a string is a palin-

drome. Use a loop invariant.

26
 5. Bubble Sort: Write bubble sort and identify its loop invariant(s).
Prove that it sorts correctly.

6. Binary Search for First Occurrence: Modify binary search to return

the first occurrence of a duplicate. Prove it using an invariant.

7. Merge Two Sorted Arrays: Given two sorted arrays, merge them into
one sorted array. Identify loop invariants for the merging process.

8. GCD (Euclidean Algorithm): Implement the Euclidean algorithm

for greatest common divisor. Prove its correctness using a loop in-
variant.

11 Conclusion
Algorithm correctness is a fundamental topic in computer science. By un-
derstanding partial correctness, termination, preconditions, postconditions,
and loop invariants, you gain the ability to reason about algorithms rigor-
ously. The five-point checklist for loops provides a practical guide to ensure
your loops are correct. Remember:

A correct algorithm is not accidental. It is proven.

We have explored numerous examples, from simple maximum find-
ing to binary search and sorting algorithms. Each example demonstrated
how to formulate invariants and prove correctness. Armed with these tech-
niques, you are now better prepared to design reliable algorithms and to
debug faulty ones.

Further Reading:

• Cormen, T. H., et al. Introduction to Algorithms (CLRS) – Chapters on

correctness and loop invariants.

• Gries, D. The Science of Programming – A classic text on program cor-

rectness.

27
• Hoare, C. A. R. ”An Axiomatic Basis for Computer Programming” –
The original paper on Hoare logic.

28