Exercises · Correctness

Exercises · Chapter 13 · each solution opens with a click · Chapter 13: Correctness · Exercises, volume 4 (PDF)

In the exercises of this chapter the correctness of a loop is proved with a loop invariant, as in the chapter «Correctness», following the scheme below.

A loop invariant is a property of the variables that is true every time the condition of the loop is evaluated. To prove the correctness of the loop:

1. Initialization: the invariant is true before the first iteration;

2. Maintenance: if the invariant is true before an iteration, it is true before the next one;

3. Termination: the loop terminates after a finite number of iterations (a natural number strictly decreases at each iteration), and the invariant, together with the negated condition of the loop, gives the correct output.

A sub-array \(a[l..r]\) with \(l>r\) is empty, and an empty sum is equal to \(0\). To show that an algorithm is wrong, one counterexample is enough.

Exercise 13.1: Correctness (E1)

Consider the following algorithm, which computes the minimum value of an array \(a[1..n]\) of \(n\ge 1\) natural numbers.

Algorithm: FindMinimum

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

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

1function FindMinimum(a, n)

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

3\(i := 2\)

4while \(i \leq n\) do

5if \(a[i] < min\) then

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

7end

8\(i \leftarrow i + 1\)

9end

10return \(min\)

11end

Questions

1. State a loop invariant for the while loop of FindMinimum.

2. Verify the loop invariant on the array \(a=[7,3,9,2,5,2]\), showing the values of \(i\) and \(min\) every time the condition at line 4 is evaluated.

3. Prove the correctness of FindMinimum (initialization, maintenance, termination).

4. A student replaces line 2 with \(min := 0\). Show, with a counterexample, that the new algorithm is wrong, and indicate which property of the loop invariant fails.

Solution

1. Loop invariant:

   Every time the condition at line 4 is evaluated,

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

2. For \(a=[7,3,9,2,5,2]\) (\(n=6\)):

   \(i\)	\(min\)	\(a[1..i-1]\)	\(\min\{a[1],\dots,a[i-1]\}\)
   2	7	\([7]\)	7
   3	3	\([7,3]\)	3
   4	3	\([7,3,9]\)	3
   5	2	\([7,3,9,2]\)	2
   6	2	\([7,3,9,2,5]\)	2
   7	2	\([7,3,9,2,5,2]\)	2 (loop ends)

   The invariant holds at every evaluation, and the algorithm returns \(2\).

3. Proof of correctness.

   • Initialization. Before the first iteration \(min=a[1]\) and \(i=2\). The sub-array \(a[1..1]\) has the single element \(a[1]\), whose minimum is \(a[1]=min\).

   • Maintenance. Assume \(min=\min\{a[1],\dots,a[i-1]\}\) and \(i\le n\). If \(a[i]<min\), line 6 sets \(min\leftarrow a[i]\), which is smaller than all the elements of \(a[1..i-1]\); otherwise \(min\le a[i]\) and \(min\) is not changed. In both cases \(min=\min\{a[1],\dots,a[i]\}\). Line 8 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, so the loop terminates after \(n-1\) iterations, when \(i=n+1\). Substituting \(i=n+1\) in the invariant:

     \[ min=\min\{a[1],\dots,a[n]\}, \]

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

4. With \(min:=0\), consider \(a=[3,5]\). Since no element is smaller than \(0\), line 6 is never executed and the algorithm returns \(0\), while the correct output is \(3\). Hence the algorithm is wrong.

   The property that fails is the initialization: before the first iteration \(i=2\) and \(min=0\), while \(\min\{a[1]\}=a[1]=3\neq 0\). Maintenance is still true (if the invariant held, it would continue to hold), but since it is false at the beginning, the termination argument cannot be applied. In fact, since the entries are natural numbers, the algorithm always returns \(\min\{0,a[2],\dots,a[n]\}=0\), which is correct only if at least one entry of the array is equal to \(0\).

Exercise 13.2: Correctness (E2)

Consider the following algorithm.

Algorithm: ArraySum

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

Output: A natural number \(s\)

1function ArraySum(a, n)

2\(s := 0\)

3\(i := 1\)

4while \(i \leq n\) do

5\(s \leftarrow s + a[i]\)

6\(i \leftarrow i + 1\)

7end

8return \(s\)

9end

Questions

1. What does the algorithm compute? State a loop invariant for its while loop.

2. Verify the loop invariant on the array \(a=[4,1,7,3]\), showing the values of \(i\) and \(s\) every time the condition at line 4 is evaluated.

3. Prove the correctness of ArraySum.

4. A student modifies line 3 into \(i:=0\) and line 4 into “while \(i<n\)”, keeping \(a[i]\) at line 5. Is the new algorithm correct?

Solution

1. The algorithm computes the sum of the elements of the array:

   \[ s=\sum_{k=1}^{n}a[k]. \]

   Loop invariant:

   Every time the condition at line 4 is evaluated,

   \[ s=\sum_{k=1}^{i-1}a[k], \]

   where an empty sum (\(i=1\)) is equal to \(0\).

2. For \(a=[4,1,7,3]\) (\(n=4\)):

   \(i\)	\(s\)	\(\sum_{k=1}^{i-1}a[k]\)
   1	0	\(0\) (empty sum)
   2	4	\(4\)
   3	5	\(4+1=5\)
   4	12	\(4+1+7=12\)
   5	15	\(4+1+7+3=15\) (loop ends)

   The algorithm returns \(15\).

3. Proof of correctness.

   • Initialization. Before the first iteration \(s=0\) and \(i=1\); the sum \(\sum_{k=1}^{0}a[k]\) is empty, hence equal to \(0=s\).

   • Maintenance. Assume \(s=\sum_{k=1}^{i-1}a[k]\) and \(i\le n\). Line 5 gives

     \[ s+a[i]=\sum_{k=1}^{i-1}a[k]+a[i]=\sum_{k=1}^{i}a[k], \]

     and line 6 increases \(i\) by \(1\), so the invariant holds with the new value of \(i\).

   • Termination. The variable \(i\) starts from \(1\) and increases by \(1\) at every iteration, so the loop terminates after \(n\) iterations, when \(i=n+1\). Substituting \(i=n+1\) in the invariant gives \(s=\sum_{k=1}^{n}a[k]\), which is returned at line 8. Hence the algorithm is correct.

4. No. With \(i:=0\) the first iteration accesses \(a[0]\), which does not exist in an array \(a[1..n]\); moreover, the condition \(i<n\) stops the loop when \(i=n\), so \(a[n]\) is never added. In terms of the invariant, the natural invariant of the new loop is \(s=\sum_{k=0}^{i-1}a[k]\), and at termination (\(i=n\)) it gives \(s=\sum_{k=0}^{n-1}a[k]\neq\sum_{k=1}^{n}a[k]\): the termination step does not give the required property. For example, on \(a=[4,1,7,3]\) the element \(a[4]=3\) is never added, so even ignoring the invalid access the result cannot be \(15\). This is a typical error obtained by mixing \(0\)-indexed code (as in C++) with \(1\)-indexed pseudo-code.

Exercise 13.3: Correctness (E3)

Consider the SelectionSort algorithm, which sorts an array \(a[1..n]\) of \(n\ge 1\) natural numbers in non-decreasing order.

Algorithm: SelectionSort

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

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

1function SelectionSort(a, n)

2\(i := 1\)

3while \(i \le n-1\) do

4\(\mathit{minIdx} := i\)// index of the minimum in \(a[i..n]\)

5\(j := i+1\)

6while \(j \le n\) do

7if \(a[j] < a[\mathit{minIdx}]\) then

8\(\mathit{minIdx} \leftarrow j\)// new minimum found

9end

10\(j \leftarrow j + 1\)

11end

12if \(\mathit{minIdx} \neq i\) then

13\(\mathit{tmp} \leftarrow a[i]\)// swap \(a[i]\) and \(a[\mathit{minIdx}]\)

14\(a[i] \leftarrow a[\mathit{minIdx}]\)

15\(a[\mathit{minIdx}] \leftarrow \mathit{tmp}\)

16end

17\(i \leftarrow i + 1\)

18end

19end

Questions

1. State a loop invariant for the inner while loop (line 6) and prove it.

2. State a loop invariant for the outer while loop (line 3).

3. Verify the invariant of the outer loop on the array \(a=[29,10,14,37,13]\).

4. Prove the correctness of SelectionSort.

Solution

1. Consider an iteration of the outer loop with a given value of \(i\). The inner loop does not modify the array. Its invariant is:

   Every time the condition at line 6 is evaluated, \(i\le \mathit{minIdx}\le j-1\) and

   \[ a[\mathit{minIdx}]=\min\{a[i],a[i+1],\dots,a[j-1]\}. \]

   • Initialization. Lines 4–5 set \(\mathit{minIdx}=i\) and \(j=i+1\): the sub-array \(a[i..j-1]=a[i..i]\) has the single element \(a[i]=a[\mathit{minIdx}]\).

   • Maintenance. Assume the invariant and \(j\le n\). If \(a[j]<a[\mathit{minIdx}]\), then \(a[j]\) is smaller than all the elements of \(a[i..j-1]\) and line 8 sets \(\mathit{minIdx}\leftarrow j\); otherwise \(a[\mathit{minIdx}]\le a[j]\). In both cases \(a[\mathit{minIdx}]=\min\{a[i],\dots,a[j]\}\) and \(i\le\mathit{minIdx}\le j\). Line 10 sets \(j\leftarrow j+1\), so the invariant holds with the new \(j\).

   • Termination. \(j\) increases by \(1\) from \(i+1\le n\), so the loop stops when \(j=n+1\). Then \(a[\mathit{minIdx}]=\min\{a[i],\dots,a[n]\}\): \(\mathit{minIdx}\) is the index of a minimum element of \(a[i..n]\).

2. Invariant of the outer loop:

   Every time the condition at line 3 is evaluated:

   • (P1) the array \(a[1..n]\) contains the original elements (it is a rearrangement of the input);

   • (P2) the sub-array \(a[1..i-1]\) is sorted in non-decreasing order;

   • (P3) every element of \(a[1..i-1]\) is \(\le\) every element of \(a[i..n]\).

3. For \(a=[29,10,14,37,13]\) (\(n=5\)); the sorted prefix \(a[1..i-1]\) is highlighted in blue:

   \(i\)	\(a[1]\)	\(a[2]\)	\(a[3]\)	\(a[4]\)	\(a[5]\)	minimum of \(a[i..n]\)
   1	29	10	14	37	13	\(a[2]=10\): swap \(a[1],a[2]\)
   2	10	29	14	37	13	\(a[5]=13\): swap \(a[2],a[5]\)
   3	10	13	14	37	29	\(a[3]=14\): no swap
   4	10	13	14	37	29	\(a[5]=29\): swap \(a[4],a[5]\)
   5	10	13	14	29	37	loop ends (\(i=n\))

   At every row the blue prefix is sorted, and each blue element is \(\le\) every non-blue element: e.g. for \(i=4\), \(\max\{10,13,14\}=14\le\min\{37,29\}=29\).

4. Proof of correctness.

   • Initialization. Before the first iteration \(i=1\) and nothing has been modified: (P1) holds, and \(a[1..0]\) is empty, so (P2) and (P3) hold trivially.

   • Maintenance. Assume (P1)–(P3) and \(i\le n-1\). By point 1, after the inner loop

     \[ a[\mathit{minIdx}]=\min\{a[i],\dots,a[n]\}. \]

     Lines 12–15 swap \(a[i]\) and \(a[\mathit{minIdx}]\) (if they are different positions). A swap only exchanges two elements, so (P1) still holds. Now \(a[i]\) is the minimum of \(a[i..n]\), so:

     • by (P3), \(a[i]\ge\) every element of \(a[1..i-1]\), and since \(a[1..i-1]\) is sorted (P2), \(a[1..i]\) is sorted;

     • \(a[i]\le\) every element of \(a[i+1..n]\), because \(a[i]\) is the minimum of \(a[i..n]\) and the swap only rearranges the values in positions \(i..n\); for the same reason, by (P3) every element of \(a[1..i-1]\) is \(\le\) every element of \(a[i+1..n]\). Hence every element of \(a[1..i]\) is \(\le\) every element of \(a[i+1..n]\).

     Line 17 sets \(i\leftarrow i+1\), so (P1)–(P3) hold with the new value of \(i\).

   • Termination. The inner loop always terminates (point 1), and \(i\) increases by \(1\) from \(1\); the outer loop stops when \(i=n\) for the first time (after \(n-1\) iterations; if \(n=1\) it is never executed and \(i=1=n\)). Substituting \(i=n\): \(a[1..n-1]\) is sorted (P2) and every element of \(a[1..n-1]\) is \(\le a[n]\) (P3); hence the whole array \(a[1..n]\) is sorted and, by (P1), it contains the original elements. Hence the algorithm is correct.

   Note that the outer loop needs only \(n-1\) iterations: when the first \(n-1\) positions are correct, the last element is automatically in its correct position.

Exercise 13.4: Correctness (E4)

Consider the LinearSearch algorithm, which determines if a target value \(m\) is one of the elements of an array \(a[1..n]\) of \(n\) natural numbers (not necessarily sorted).

Algorithm: LinearSearch

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

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

1function LinearSearch(a, n, m)

2\(i := 1\)

3while \(i \le n\) do

4if \(a[i] = m\) then

5return \(i\)// Element found at index \(i\)

6end

7\(i \leftarrow i + 1\)

8end

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

10end

Questions

1. State a loop invariant for the while loop of LinearSearch.

2. Verify the loop invariant on the array \(a=[8,3,6,3,9]\) for \(m=6\) and for \(m=5\).

3. Prove that LinearSearch is correct. Prove also that, when \(m\) is in the array, the returned index is the smallest index \(k\) such that \(a[k]=m\).

4. A student swaps lines 4–5 and line 7, i.e., the body of the loop first increases \(i\) and then checks whether \(a[i]=m\). Find a counterexample showing that the new algorithm is wrong, and indicate which property of the loop invariant fails.

Solution

1. Loop invariant:

   Every time the condition at line 3 is evaluated, \(1\le i\le n+1\) and \(m\) is not in the sub-array \(a[1..i-1]\):

   \[ a[k]\neq m\qquad \text{for every } k\in\{1, 2, \dots, i-1\}. \]

2. For \(a=[8,3,6,3,9]\):

   \(m\)	\(i\)	\(a[1..i-1]\)	action
   6	1	\([\ ]\)	\(a[1]=8\neq 6\)
   	2	\([8]\)	\(a[2]=3\neq 6\)
   	3	\([8,3]\)	\(a[3]=6=m\) \(\Rightarrow\) return \(3\)
   5	1	\([\ ]\)	\(a[1]=8\neq 5\)
   	2	\([8]\)	\(a[2]=3\neq 5\)
   	3	\([8,3]\)	\(a[3]=6\neq 5\)
   	4	\([8,3,6]\)	\(a[4]=3\neq 5\)
   	5	\([8,3,6,3]\)	\(a[5]=9\neq 5\)
   	6	\([8,3,6,3,9]\)	\(i>n\) \(\Rightarrow\) return \(-1\)

   At every evaluation, \(m\) does not appear in \(a[1..i-1]\).

3. Proof of correctness.

   • Initialization. Before the first iteration \(i=1\) and \(a[1..0]\) is empty, so it does not contain \(m\).

   • Maintenance. Assume the invariant and \(i\le n\). If \(a[i]=m\), the algorithm returns \(i\) (line 5), which is a correct output. Otherwise \(a[i]\neq m\), so \(m\) is not in \(a[1..i]\); line 7 sets \(i\leftarrow i+1\) and the invariant holds with the new value of \(i\).

   • Termination. \(i\) increases by \(1\) from \(1\), so the loop executes at most \(n\) iterations. The algorithm ends in one of two ways:

     • it returns \(i\) with \(a[i]=m\): correct. Moreover, by the invariant \(a[k]\neq m\) for all \(k<i\), so \(i\) is the smallest index with \(a[i]=m\);

     • the condition at line 3 is false, i.e., \(i=n+1\): by the invariant \(m\) is not in \(a[1..n]\), and the algorithm correctly returns \(-1\).

     Hence the algorithm is correct.

4. The new body is: \(i\leftarrow i+1\); if \(a[i]=m\) then return \(i\). Consider \(a=[6,3]\) and \(m=6\). In the first iteration \(i\) becomes \(2\) and \(a[2]=3\neq 6\); in the second iteration \(i\) becomes \(3\) and the algorithm accesses \(a[3]\), which is outside the array; in any case \(a[1]=6\) is never checked, so the algorithm cannot return \(1\).

   The property that fails is the maintenance: if \(m\) is not in \(a[1..i-1]\) at the beginning of the iteration, after the body we only know that \(m\) is not in \(a[1..i-1]\) and that \(a[i+1]\neq m\), but nothing is known about \(a[i]\). With the new value \(i+1\), the invariant would require \(m\) not in \(a[1..i]\), which is not guaranteed: in the example, before the second evaluation of the condition \(i=2\) and \(a[1]=6=m\).

Exercise 13.5: Correctness (E5)

Consider the following two algorithms, which should compute \(x^n\) for two natural numbers \(x\ge 1\) and \(n\ge 0\) (recall that \(x^0=1\)).

Algorithm: Power

Input: Two natural numbers \(x\ge 1\) and \(n\ge 0\)

Output: \(x^n\)

1function Power(x, n)

2\(p := 1\)

3\(i := 1\)

4while \(i \leq n\) do

5\(p \leftarrow p \cdot x\)

6\(i \leftarrow i + 1\)

7end

8return \(p\)

9end

Algorithm: WrongPower

Input: Two natural numbers \(x\ge 1\) and \(n\ge 0\)

Output: \(x^n\) (?)

1function WrongPower(x, n)

2\(p := x\)

3\(i := 1\)

4while \(i \leq n\) do

5\(p \leftarrow p \cdot x\)

6\(i \leftarrow i + 1\)

7end

8return \(p\)

9end

Questions

1. State a loop invariant for the while loop of Power and verify it for \(x=3\), \(n=4\).

2. Prove the correctness of Power, including the case \(n=0\).

3. Show that the same invariant is not a loop invariant of WrongPower: which of the three properties fails? Give a counterexample showing that WrongPower is wrong, with a trace for \(x=2\), \(n=3\).

4. Find the correct loop invariant of WrongPower and use it to determine exactly what WrongPower computes. For which inputs is its output correct?

Solution

1. Loop invariant of Power:

   Every time the condition at line 4 is evaluated, \(1\le i\le n+1\) and

   \[ p=x^{\,i-1}. \]

   For \(x=3\), \(n=4\):

   \(i\)	\(p\)	\(x^{i-1}\)
   1	1	\(3^0=1\)
   2	3	\(3^1=3\)
   3	9	\(3^2=9\)
   4	27	\(3^3=27\)
   5	81	\(3^4=81\) (loop ends)

   The algorithm returns \(81=3^4\).

2. Proof of correctness of Power.

   • Initialization. Before the first iteration \(p=1\) and \(i=1\), so \(p=x^0=x^{i-1}\); moreover \(1\le i\le n+1\) since \(n\ge 0\).

   • Maintenance. Assume \(p=x^{i-1}\) and \(i\le n\). Line 5 gives \(p\cdot x=x^{i-1}\cdot x=x^{i}\), and line 6 sets \(i\leftarrow i+1\le n+1\). With the new value of \(i\), \(p=x^{i-1}\).

   • Termination. \(i\) increases by \(1\) from \(1\le n+1\), so the loop terminates after exactly \(n\) iterations, when \(i=n+1\). Substituting \(i=n+1\): \(p=x^{n}\), which is returned at line 8.

   If \(n=0\), the condition \(1\le 0\) is false at the first evaluation, the loop is never executed and the algorithm returns \(p=1=x^0\), in agreement with the proof (initialization and termination coincide, with \(i=1=n+1\)).

3. For WrongPower, the initialization fails: before the first iteration \(i=1\) and \(p=x\), while \(x^{i-1}=x^0=1\). Hence \(p\neq x^{i-1}\) whenever \(x\ge 2\). (Maintenance is still true: if \(p=x^{i-1}\) held, the body would preserve it; but the “induction” has no valid base case.)

   Counterexample: \(x=2\), \(n=3\), for which \(x^n=8\).

   \(i\)	\(p\)	\(x^{i-1}\)	\(x^{i}\)
   1	2	1	2
   2	4	2	4
   3	8	4	8
   4	16	8	16 (loop ends)

   WrongPower returns \(16\neq 8=2^3\), so it is wrong.

4. The table suggests the invariant \(p=x^{\,i}\), which is a correct loop invariant of WrongPower:

   • Initialization: \(p=x=x^1=x^i\) with \(i=1\);

   • Maintenance: if \(p=x^i\) and \(i\le n\), after the body \(p=x^{i+1}\) and \(i\) is increased by \(1\);

   • Termination: the loop ends with \(i=n+1\), so \(p=x^{n+1}\).

   Therefore WrongPower computes \(x^{n+1}\). Its output is correct, i.e., \(x^{n+1}=x^n\), if and only if \(x^n(x-1)=0\), that is (since \(x\ge 1\)) if and only if \(x=1\). For every \(x\ge 2\) and every \(n\ge 0\) it is wrong: one counterexample is enough to show that an algorithm is not correct.