Correctness

Part 4 · Analysis of algorithms · Chapter 13 · Lecture notes, volume 4 (PDF) · Exercises: Correctness · App: The loop invariant

13.1 Correctness of an algorithm

• The previous chapters measured how much an algorithm costs: the size of its input and its running time. Before asking how fast an algorithm is, however, we must be sure that it does what it promises. This chapter presents the standard tool to prove it, the loop invariant, and applies it to algorithms already met in the chapters «Sorting», «Linear and binary search» and «Numerical algorithms»: Find Maximum, Insertion Sort, Binary Search and the Euclidean algorithm.

• The first part of the analysis of an algorithm consists in determining its correctness, i.e., proving that it computes the correct output for every possible input instance.

• Testing an algorithm on some instances can show that it is wrong (one counterexample is enough), but it can never show that it is correct: there are infinitely many input instances. Correctness must be proved.

Definition 13.1: correct algorithm

An algorithm is correct if, for every input instance \(I\) of the problem, it terminates after a finite number of steps and it returns the correct output for \(I\).

• The algorithms we consider consist of sequences of instructions and of loops. Sequences of instructions are easy to analyse, while a loop executes the same instructions a number of times that depends on the input.

The correctness of an algorithm is based on the correctness of its loops. The correctness of a loop is proved by means of a loop invariant.

13.1.1 Loop invariants

Definition 13.2: loop invariant

A loop invariant is a property of the variables of an algorithm that is true every time the condition of a loop is evaluated, i.e., before the first iteration of the loop and after each iteration of the loop.

• To prove the correctness of an algorithm by means of a loop invariant, we must show three things:

  1. Initialization: the loop invariant is true before the first iteration of the loop.

  2. Maintenance: if the loop invariant is true before an iteration of the loop, then it remains true at the end of the iteration, or equivalently, it is true before the next iteration.

  3. Termination: the loop terminates after a finite number of iterations. When the loop terminates, the loop invariant, together with the fact that the condition of the loop is false, gives a useful property that shows that the algorithm is correct.

• Note the similarity with mathematical induction, where to prove that a property holds it is necessary to prove a base case and an inductive step:

  • showing that the invariant holds before the first iteration corresponds to the base case;

  • showing that the invariant holds from iteration to iteration corresponds to the inductive step.

  The termination property differs from the usual use of mathematical induction, in which the inductive step is applied infinitely many times: here, we stop the “induction” when the loop terminates.

• To prove that a loop terminates, we usually identify a natural number (for example, \(n-i+1\) or the length of a sub-array) that strictly decreases at every iteration and that must be positive for the loop to continue. Since a natural number cannot decrease forever, the loop terminates.

Scheme of a correctness proof with a loop invariant

1. State the invariant: a property of the variables, true every time the condition of the loop is evaluated.

2. Initialization: check it with the values assigned before the loop.

3. Maintenance: assume it and the condition of the loop, execute the body once, and check it with the new values.

4. Termination: find a natural number that strictly decreases at each iteration; then combine the invariant with the negated condition of the loop to obtain the correct output.

13.2 Correctness of Find Maximum

Given an array \(a[1..n]\) of \(n\) integer numbers, with \(n \ge 1\), consider the problem of determining the maximum value in the array.

• The first example is the simplest loop: a single scan of the array. This is the pseudo-code of the FindMaximum algorithm.

Algorithm: FindMaximum

Input: An array \(a[1..n]\) of \(n\) integer numbers

Output: The maximum value in array \(a\)

1function FindMaximum(a, n)

2\(max := a[1]\)

3\(i := 2\)

4while \(i \leq n\) do

5if \(a[i] > max\) then

6\(max \leftarrow a[i]\)

7end

8\(i \leftarrow i + 1\)

9end

10return \(max\)

11end

Run in Colab:PythonC++Java

• The loop invariant of the while loop of FindMaximum is:

Every time the condition at line 4 is evaluated, the variable \(max\) is equal to the maximum value of the sub-array \(a[1..i-1]\):

\[ max=\max\{a[1],a[2],\dots,a[i-1]\}. \]

Example 13.1: Loop invariant of FindMaximum

Consider the array \(a=[9, 12, 3, 16, 19, 11, 12]\) with \(n=7\). The table shows the values of \(i\) and \(max\) every time the condition at line 4 is evaluated:

\(i\)	\(max\)	\(a[1..i-1]\)	\(\max\{a[1],\dots,a[i-1]\}\)
2	9	\([9]\)	9
3	12	\([9,12]\)	12
4	12	\([9,12,3]\)	12
5	16	\([9,12,3,16]\)	16
6	19	\([9,12,3,16,19]\)	19
7	19	\([9,12,3,16,19,11]\)	19
8	19	\([9,12,3,16,19,11,12]\)	19 (loop ends)

At every evaluation the invariant holds. When the loop ends \(i=n+1=8\), and the algorithm returns \(19\), the maximum of the whole array.

• Using the loop invariant we can prove the correctness of the FindMaximum algorithm, which is stated by the following observation.

Observation 13.3

Given an array \(a[1..n]\) of \(n \ge 1\) integer numbers, the FindMaximum algorithm terminates and returns

\[ \max\{a[1],a[2],\dots,a[n]\}. \]

Proof

We prove the three properties of the loop invariant.

• Initialization. Before the first iteration, lines 2 and 3 set \(max=a[1]\) and \(i=2\). The sub-array \(a[1..i-1]=a[1..1]\) consists of the single element \(a[1]\), whose maximum is \(a[1]=max\). Hence the invariant holds.

• Maintenance. Assume that, before an iteration, \(max=\max\{a[1],\dots,a[i-1]\}\). The body of the loop compares \(a[i]\) with \(max\) (line 5):

  • if \(a[i]>max\), then line 6 sets \(max \leftarrow a[i]\), and \(a[i]\) is greater than all the elements of \(a[1..i-1]\);

  • if \(a[i]\le max\), then \(max\) is not changed and it is greater than or equal to \(a[i]\).

  In both cases, at the end of the body

  \[ max=\max\{a[1],\dots,a[i-1],a[i]\}. \]

  Line 8 increases \(i\) by \(1\), so that, with the new value of \(i\), we have again \(max=\max\{a[1],\dots,a[i-1]\}\). Hence the invariant holds before the next iteration.

• Termination. The variable \(i\) starts from \(2\le n+1\) and increases by \(1\) at every iteration, therefore the loop terminates after exactly \(n-1\) iterations, when for the first time \(i=n+1\). Substituting \(i=n+1\) in the loop invariant we obtain

  \[ max=\max\{a[1],a[2],\dots,a[n]\}, \]

  which is the value returned at line 10. Hence, the algorithm is correct.

□

13.3 Correctness of Insertion Sort

Given an array \(a[1..n]\) of \(n\) natural numbers, with \(n\ge 1\), consider the problem of rearranging the elements of the array in non-decreasing order:

\[ a[1] \le a[2] \le \cdots \le a[n]. \]

• With two nested loops the proof needs two invariants, one for each loop. This is the pseudo-code of the InsertionSort algorithm.

Algorithm: InsertionSort

Input: An array \(a[1..n]\) of \(n\) natural numbers

Output: The array \(a\) sorted in non-decreasing order

1function InsertionSort(a, n)

2\(i := 2\)

3while \(i \le n\) do

4\(key := a[i]\)// Element to insert

5\(j := i - 1\)

6while \(j \ge 1\) and \(a[j] > key\) do

7\(a[j+1]\) \(\leftarrow\) \(a[j]\)// Shift element to the right

8\(j\) \(\leftarrow\) \(j - 1\)

9end

10\(a[j+1]\) \(\leftarrow\) \(key\)// Insert key in correct position

11\(i \leftarrow i + 1\)

12end

13end

Run in Colab:PythonC++Java

• The condition at line 6 is evaluated from left to right, and the second part is evaluated only if the first one is true: when \(j=0\) the condition is false and the non-existent element \(a[0]\) is never accessed.

• The algorithm contains two nested loops. We first prove what a single execution of the inner while loop (lines 6–8) does, and then we use this result to prove the correctness of the outer while loop (lines 3–11).

13.3.1 The inner loop

• Consider one iteration of the outer loop, with a given value of \(i \in \{2,3,\dots,n\}\). We denote by

  \[ b[1..i] \]

  the content of the sub-array \(a[1..i]\) at the beginning of this iteration (i.e., when the condition at line 3 is true), and we assume that \(b[1..i-1]\) is sorted in non-decreasing order. After line 4 we have \(key=b[i]\).

• The loop invariant of the inner while loop is:

Every time the condition at line 6 is evaluated:

• (I1) \(a[1..j]=b[1..j]\) (the first \(j\) elements have not been moved);

• (I2) \(a[j+2..i]=b[j+1..i-1]\) (the elements \(b[j+1],\dots,b[i-1]\) have been shifted one position to the right);

• (I3) every element of \(a[j+2..i]\) is strictly greater than \(key\).

The entries \(a[i+1..n]\) are never modified by the inner loop.

• The position \(j+1\) is the “hole” in which \(key\) will be inserted: its current content is a copy that will be overwritten. A sub-array \(a[l..r]\) with \(l>r\) is empty, and any property of all its elements is trivially true.

Example 13.2: Loop invariant of the inner loop

Consider the array \(a=[5,2,4,1,3]\) at the beginning of the iteration \(i=5\) of the outer loop: \(b[1..5]=[1,2,4,5,3]\) and \(key=3\). The table shows the array every time the condition at line 6 is evaluated.

\(j\)	\(a[1]\)	\(a[2]\)	\(a[3]\)	\(a[4]\)	\(a[5]\)	\(a[1..j]\)	\(a[j+2..5]\)	condition
4	1	2	4	5	3	\([1,2,4,5]\)	\([\ ]\)	\(a[4]=5>3\): true
3	1	2	4	5	5	\([1,2,4]\)	\([5]\)	\(a[3]=4>3\): true
2	1	2	4	4	5	\([1,2]\)	\([4,5]\)	\(a[2]=2\le 3\): false

At every evaluation \(a[1..j]=b[1..j]\), \(a[j+2..5]=b[j+1..4]\) and all the elements of \(a[j+2..5]\) are greater than \(3\). When the loop ends \(j=2\), and line 10 sets \(a[3]\leftarrow 3\), giving \(a[1..5]=[1,2,3,4,5]\).

Lemma 13.4: inner loop of Insertion Sort

Consider an iteration of the outer loop of InsertionSort with \(i\in\{2,\dots,n\}\), and let \(b[1..i]\) be the content of \(a[1..i]\) at the beginning of the iteration. If \(b[1..i-1]\) is sorted in non-decreasing order, then the inner while loop terminates and, after line 10, the sub-array \(a[1..i]\) contains the elements \(b[1],\dots,b[i]\) sorted in non-decreasing order, while \(a[i+1..n]\) is unchanged.

Proof

We prove the three properties of the loop invariant (I1)–(I3).

• Initialization. Before the first evaluation of the condition, \(j=i-1\) and nothing has been modified. Hence \(a[1..i-1]=b[1..i-1]\), i.e. (I1) holds. The sub-arrays \(a[j+2..i]=a[i+1..i]\) and \(b[j+1..i-1]=b[i..i-1]\) are both empty, so (I2) and (I3) hold trivially.

• Maintenance. Assume that (I1)–(I3) hold and that the condition at line 6 is true, i.e., \(j\ge 1\) and \(a[j]>key\). By (I1), \(a[j]=b[j]\), so \(b[j]>key\). Line 7 sets \(a[j+1]\leftarrow a[j]=b[j]\); therefore, by (I2),

  \[ a[j+1..i]=b[j..i-1], \]

  and all these elements are greater than \(key\) (by (I3) and \(b[j]>key\)). Positions \(1,\dots,j\) are not modified. Line 8 sets \(j\leftarrow j-1\). Denoting by \(j'=j-1\) the new value, we have \(a[1..j']=b[1..j']\), \(a[j'+2..i]=a[j+1..i]=b[j..i-1]=b[j'+1..i-1]\), and all the elements of \(a[j'+2..i]\) are greater than \(key\). Hence (I1)–(I3) hold before the next evaluation of the condition.

• Termination. The variable \(j\) starts from \(i-1\) and decreases by \(1\) at every iteration; since the loop stops at the latest when \(j=0\), the inner loop executes at most \(i-1\) iterations and terminates. When it terminates, either \(j=0\) or \(a[j]=b[j]\le key\). By (I1)–(I3):

  • \(a[1..j]=b[1..j]\) is sorted and, if \(j\ge 1\), its largest element \(b[j]\) is \(\le key\);

  • \(a[j+2..i]=b[j+1..i-1]\) is sorted and all its elements are \(>key\).

  Line 10 sets \(a[j+1]\leftarrow key=b[i]\). Therefore

  \[ a[1..i]=\big[\,b[1],\dots,b[j],\ key,\ b[j+1],\dots,b[i-1]\,\big], \]

  which contains exactly the elements \(b[1],\dots,b[i]\) and is sorted in non-decreasing order, because \(b[1..j]\) is sorted, \(b[j]\le key< b[j+1]\), and \(b[j+1..i-1]\) is sorted. Positions \(i+1,\dots,n\) are never accessed.

□

13.3.2 The outer loop

• The loop invariant of the outer while loop is:

Every time the condition at line 3 is evaluated, the sub-array \(a[1..i-1]\) consists of the elements originally in \(a[1..i-1]\), but sorted in non-decreasing order, and the sub-array \(a[i..n]\) is equal to the original sub-array \(a[i..n]\).

Example 13.3: Loop invariant of the outer loop

Consider the array \(a=[5,2,4,1,3]\) with \(n=5\). The table shows the array every time the condition at line 3 is evaluated; the sorted sub-array \(a[1..i-1]\) is highlighted in blue.

\(i\)	\(a[1]\)	\(a[2]\)	\(a[3]\)	\(a[4]\)	\(a[5]\)	original \(a[1..i-1]\)
2	5	2	4	1	3	\([5]\)
3	2	5	4	1	3	\([5,2]\)
4	2	4	5	1	3	\([5,2,4]\)
5	1	2	4	5	3	\([5,2,4,1]\)
6	1	2	3	4	5	\([5,2,4,1,3]\) (loop ends)

• Using the loop invariant and Lemma 13.4 we can prove the correctness of the InsertionSort algorithm.

Observation 13.5

Given an array \(a[1..n]\) of \(n\ge 1\) natural numbers, the InsertionSort algorithm terminates and, at the end, the array \(a[1..n]\) contains the original elements rearranged in non-decreasing order:

\[ a[1]\le a[2]\le\cdots\le a[n]. \]

Proof

We prove the three properties of the loop invariant of the outer loop.

• Initialization. Before the first iteration, \(i=2\) (line 2) and the array has not been modified. The sub-array \(a[1..i-1]=a[1..1]\) consists of the single original element \(a[1]\), and it is trivially sorted. The sub-array \(a[2..n]\) is the original one. Hence the invariant holds.

• Maintenance. Assume that the invariant holds and that \(i\le n\). Then \(a[1..i-1]\) contains the original elements of \(a[1..i-1]\) sorted, and \(a[i]\) is the original element \(a[i]\). By Lemma 13.4, after line 10 the sub-array \(a[1..i]\) contains these \(i\) elements, i.e., the original elements of \(a[1..i]\), sorted in non-decreasing order, and \(a[i+1..n]\) is unchanged, hence still equal to the original one. Line 11 sets \(i\leftarrow i+1\), so the invariant holds with the new value of \(i\).

• Termination. The variable \(i\) starts from \(2\le n+1\) and increases by \(1\) at every iteration, and each inner loop terminates (Lemma 13.4). Therefore the outer loop terminates after exactly \(n-1\) iterations, when \(i=n+1\) for the first time. Substituting \(i=n+1\) in the loop invariant, the sub-array \(a[1..n]\), i.e., the entire array, consists of the original elements sorted in non-decreasing order. Hence, the algorithm is correct.

□

13.4 Correctness of Binary Search

Given an array \(a[1..n]\) of \(n\) natural numbers sorted in non-decreasing order and a target natural number \(m\), consider the problem of determining if \(m\) is one of the elements of the array.

• In the previous two algorithms the loop always runs until its condition becomes false. Binary search can also stop early, with a return inside the loop, and the proof must take both exits into account. This is the pseudo-code of the (iterative) BinarySearch algorithm.

Algorithm: BinarySearch

Input: An array \(a[1..n]\) of \(n\) natural numbers sorted in non-decreasing order and a target value \(m\)

Output: Index of \(m\) in \(a\), or \(-1\) if not found

1function BinarySearch(a, n, m)

2\(left\) := \(1\)// Left boundary

3\(right\) := \(n\)// Right boundary

4while \(left \le right\) do

5\(mid\) := \(left + \lfloor (right - left) / 2 \rfloor\)// Middle index

6if \(a[mid] = m\) then

7return \(mid\)// Element found

8end

9if \(a[mid] < m\) then

10\(left\) \(\leftarrow\) \(mid + 1\)// Search in right half

11end

12else

13\(right\) \(\leftarrow\) \(mid - 1\)// Search in left half

14end

15end

16return \(-1\)// Element not found

17end

Run in Colab:PythonC++Java

• The loop invariant of the while loop of BinarySearch is:

Every time the condition at line 4 is evaluated:

• (I1) \(1\le left\) and \(right\le n\);

• (I2) if \(m\) is in \(a\), then \(m\) is in \(a[left..right]\), that is,

  \[ m\in\{a[1],\dots,a[n]\} \ \Longrightarrow\ m\in\{a[left],\dots,a[right]\}. \]

• In words: the algorithm never discards a portion of the array that may contain \(m\). The sub-array \(a[left..right]\) is called the search interval and it contains \(right-left+1\) elements (it is empty if \(left>right\)).

Example 13.4: Loop invariant of BinarySearch

Search for \(m=10\) in \(a=[3, 9, 11, 12, 12, 16, 19]\) (\(n=7\)). The table shows the search interval every time the condition at line 4 is evaluated.

\(left\)	\(right\)	\(a[left..right]\)	action
1	7	\([3,9,11,12,12,16,19]\)	\(mid=4\), \(a[4]=12>10\) \(\Rightarrow\) \(right=3\)
1	3	\([3,9,11]\)	\(mid=2\), \(a[2]=9<10\) \(\Rightarrow\) \(left=3\)
3	3	\([11]\)	\(mid=3\), \(a[3]=11>10\) \(\Rightarrow\) \(right=2\)
3	2	\([\ ]\)	\(left>right\) \(\Rightarrow\) return \(-1\)

Since \(10\) is not in \(a\), the invariant (I2) is trivially true; when the interval becomes empty the algorithm correctly returns \(-1\).

Observation 13.6

Given an array \(a[1..n]\) of \(n\) natural numbers sorted in non-decreasing order and a natural number \(m\), the BinarySearch algorithm terminates; it returns an index \(k\) such that \(a[k]=m\) if \(m\) is in \(a\), and it returns \(-1\) otherwise.

Proof

We prove the three properties of the loop invariant.

• Initialization. Lines 2 and 3 set \(left=1\) and \(right=n\). Then (I1) holds, and \(a[left..right]=a[1..n]\) is the whole array, so (I2) holds.

• Maintenance. Assume that (I1)–(I2) hold and that \(left\le right\). Line 5 computes \(mid=left+\lfloor(right-left)/2\rfloor\); since \(0\le \lfloor(right-left)/2\rfloor\le right-left\), we have

  \[ 1\le left\le mid\le right\le n, \]

  so \(a[mid]\) is a valid entry of the array. Three cases are possible.

  • \(a[mid]=m\): the algorithm returns \(mid\) at line 7, which is a correct output.

  • \(a[mid]<m\): since the array is sorted, for every \(k\le mid\) we have \(a[k]\le a[mid]<m\). Hence \(m\) is not in \(a[left..mid]\), and if \(m\) is in \(a[left..right]\) then it is in \(a[mid+1..right]\). Line 10 sets \(left\leftarrow mid+1\ge 1\), so (I1) and (I2) still hold.

  • \(a[mid]>m\): since the array is sorted, for every \(k\ge mid\) we have \(a[k]\ge a[mid]>m\). Hence, if \(m\) is in \(a[left..right]\), then it is in \(a[left..mid-1]\). Line 13 sets \(right\leftarrow mid-1\le n\), so (I1) and (I2) still hold.

• Termination. Consider the number of elements of the search interval, \(right-left+1\). In the second case the new number is \(right-mid\le right-left\), in the third case it is \(mid-left\le right-left\): in both cases it decreases by at least \(1\). Since the loop continues only while \(right-left+1\ge 1\), the loop terminates after at most \(n\) iterations. The algorithm ends in one of two ways:

  • it returns \(mid\) with \(a[mid]=m\), which is correct;

  • the condition \(left\le right\) is false, i.e., the search interval \(a[left..right]\) is empty. Since an empty sub-array does not contain \(m\), by (I2) \(m\) is not in \(a\), and the algorithm correctly returns \(-1\) at line 16.

  Hence, the algorithm is correct.

□

13.5 Correctness of the Euclidean algorithm

Given two natural numbers \(n, m \ge 1\), consider the problem of computing their greatest common divisor \(\gcd(n,m)\).

• In the last example the invariant is not a property of a portion of an array, but an equality between two numbers that never changes. This is the pseudo-code of the Euclidean algorithm.

Algorithm: EuclideanAlgorithm

Input: Two natural numbers \(n, m \ge 1\)

Output: \(\gcd(n, m)\)

1function EuclideanAlgorithm(\(n\), \(m\))

2while \(m \ne 0\) do

3\(r := n \bmod m\)

4\(n \leftarrow m\)

5\(m \leftarrow r\)

6end

7return \(n\)// \(m = 0\): \(n\) is the GCD

8end

Run in Colab:PythonC++Java

• The proof is based on the following property of the greatest common divisor, proved in the chapter «Numerical algorithms»:

  \[ \gcd(n, m) = \gcd(m,\ n \bmod m)\qquad \text{for every } n\ge 1,\ m \ge 1. \]

• We also use the convention \(\gcd(n,0)=n\) for \(n\ge 1\): every natural number divides \(0\), so the common divisors of \(n\) and \(0\) are the divisors of \(n\), and the greatest of them is \(n\).

• We denote by \(n_0\) and \(m_0\) the values of \(n\) and \(m\) given in input. The loop invariant of the while loop is:

Every time the condition at line 2 is evaluated, \(n\ge 1\), \(m\ge 0\), and

\[ \gcd(n,m)=\gcd(n_0,m_0). \]

Example 13.5: Loop invariant of the Euclidean algorithm

Consider \(n_0=252\) and \(m_0=105\). The table shows the values of \(n\) and \(m\) every time the condition at line 2 is evaluated:

\(n\)	\(m\)	\(\gcd(n,m)\)
252	105	21
105	42	21
42	21	21
21	0	21 (loop ends)

The value \(\gcd(n,m)=21\) never changes, and when \(m=0\) the algorithm returns \(n=21=\gcd(252,105)\).

Observation 13.7

Given two natural numbers \(n_0,m_0\ge 1\), the EuclideanAlgorithm terminates and returns \(\gcd(n_0,m_0)\).

Proof

We prove the three properties of the loop invariant.

• Initialization. Before the first iteration \(n=n_0\ge 1\) and \(m=m_0\ge 1\), so trivially \(\gcd(n,m)=\gcd(n_0,m_0)\).

• Maintenance. Assume that the invariant holds and that \(m\ne 0\), i.e., \(m\ge 1\). Line 3 computes \(r=n\bmod m\), with \(0\le r<m\). Lines 4–5 replace the pair \((n,m)\) with \((m,r)\). The new value of \(n\) is \(m\ge 1\), the new value of \(m\) is \(r\ge 0\), and, since \(n,m\ge 1\),

  \[ \gcd(m,r)=\gcd(m,\ n\bmod m)=\gcd(n,m)=\gcd(n_0,m_0). \]

  Hence the invariant holds before the next iteration.

• Termination. At every iteration the value of \(m\) is replaced by \(r<m\), so \(m\) is a natural number that strictly decreases. Therefore the loop terminates after at most \(m_0\) iterations, when \(m=0\). Substituting \(m=0\) in the loop invariant we obtain

  \[ \gcd(n_0,m_0)=\gcd(n,0)=n, \]

  which is the value returned at line 7. Hence, the algorithm is correct.

□

• The proof does not use the assumption \(n_0\ge m_0\): if \(n_0<m_0\), then \(n_0\bmod m_0=n_0\) and the first iteration simply swaps the two numbers.

• The bound “at most \(m_0\) iterations” is enough to prove termination, but it is very pessimistic: the number of iterations is actually \(O(\log_2 m_0)\) (in the example, \(3\) iterations for \(m_0=105\)).

13.6 Correctness of recursive algorithms

• Loop invariants are the tool to prove the correctness of iterative algorithms, i.e., algorithms based on loops.

• A recursive algorithm solves an instance of a problem by calling itself on one or more smaller instances. Its correctness is proved directly by mathematical induction on the size of the instance:

  • base case: the algorithm returns the correct output on the smallest instances, which are solved without recursive calls;

  • inductive step: under the inductive hypothesis that the recursive calls return the correct output on the smaller instances, the algorithm combines their results into the correct output for the current instance.

• Termination follows from the fact that every recursive call is made on a strictly smaller instance, so the base case is eventually reached.

The correctness of recursive algorithms is proved by induction on the size of the input. This technique is applied together with the study of recursive algorithms.

Key points of the chapter

• An algorithm is correct if, for every input instance, it terminates and returns the correct output; testing can only show that an algorithm is wrong.

• The correctness of a loop is proved with a loop invariant: initialization, maintenance and termination.

• The invariant, together with the negated condition of the loop, gives the output: \(i=n+1\) for Find Maximum and Insertion Sort, an empty search interval for Binary Search, \(m=0\) for the Euclidean algorithm.

• Nested loops need one invariant for each loop (Insertion Sort); a return inside the loop is a second exit that must be proved correct (Binary Search).

• Recursive algorithms are proved correct by induction on the size of the input.

---

Exercises on this chapter: Correctness

Interactive lab

The algorithm of the chapter, one step at a time: move the sliders and press ▶. The same graph full page, with the other ones of the course, is in the interactive lab.