This document contain relatively polished proofs with less motivation and context compared to the slides, intended only for quick reference. Please refer to the slides for the best learning experience.
Definition. An algorithm is said to be correct for a given specification if it satisfies:
Definition. A loop invariant is a property that is true right before the loop starts, and after every iteration.
Loop invariants are useful because they are properties of algorithms that are relatively easy to prove. First, prove that it is true before the loop starts. Then prove that whenever it is true before, it stays true in the next iteration. This way, it stays true forever as desired.
Algorithm.
Input: Array A[1\dots
n] of numbers
Goal: The sum of the elements in A.
1. Let sum = 0.
2. for i = 1, ..., n do
3. Update sum = sum + A[i].
4. return sumClaim. No exceptions.
Proof. The only line that can raise an exception is array access in line 3. By line 2, we have 1 \le i \le n during line 3, so we are good. ∎
Claim. Loops terminate.
Proof. For-loops always terminate. ∎
Claim. Meets specification.
Proof. We need to show that \texttt{sum} = A[1] + \dots + A[n]. Because it’s hard to show this directly, we use the loop invariant technique. We claim that after iteration i, \texttt{sum} = A[1] + \dots + A[i]. By applying this when i = n, we get the desired claim.
Before the loop starts: We set \texttt{sum} = 0, which is the sum of an empty array.
After iteration i: The previous iteration left us with \texttt{sum} = A[1] + \dots + A[i-1]. In iteration i, we add A[i] to \texttt{sum}. Thus, at the end, \texttt{sum} = A[1] + \dots + A[i-1]. ∎
Algorithm.
Input: Array A[1\dots
n] of numbers
Goal: The largest number in A (defiend as -\inf if A is empty)
1. Let max = -inf
2. for i = 1, ..., n do
3. if max < A[i] then
4. Update max = A[i]
5. return maxClaim. No exceptions.
Proof. Array access in lines 3-4 are within bounds, because line 2 gives 1 \le i \le n. ∎
Claim. Loops terminate.
Proof. For-loops always terminate. ∎
Claim. Meets specification.
Proof. Need to show that at the end of the program, \texttt{max} holds the largest number in the array A. We will use the loop invariant technique and instead show that at the end of iteration i, \texttt{max} holds the largest number in the subarray A[1 \dots i].
Before the loop starts: The largest number in the empty subarray A[1 \dots 0] is defined to be -\inf, and we start with \texttt{max} = -\inf.
After iteration i: By the previous iteration, \texttt{max} starts out holding the largest number in A[1 \dots i-1]. The largest number of A[1 \dots n] is either in A[1 \dots i-1] or is A[i].
Case 1: If the largest number of A[1 \dots n] is in A[1 \dots i-1], then by the invariant on the previous iteration, we know that \texttt{max} \ge A[i]. So we don’t enter the if statement and \texttt{max} stays the same, which is correct.
Case 2: If the largest number of A[1 \dots n] is A[i], then again by the invariant on the previous iteration, \texttt{max} < A[i]. So we enter the if statement and correctly update \texttt{max} to be A[i]. ∎
Algorithm.
Input: Array A[1\dots
n] of numbers
Goal: A permutation of A that is sorted in decreasing
order
1. for i = 1, ..., n do
2. Let A[j] be the maximum element of A[i...n]
3. Swap A[i] and A[j].
4. return AClaim. No exceptions.
Proof. Array access on i is within bounds because 1 \le i \le n. Maximum element A[j] exists because i \ge 1, so A[1 \dots i] is nonempty. ∎
Claim. Loops terminate.
Proof. For-loops always terminate. ∎
Claim. Meets specification.
Proof. We are to show that the output is a permutation of the original that is sorted in decreasing order. To show the first part, that the output is a permutation, we use the loop invariant technique.
Before the loop starts: A is unchanged, thus trivially a permutation of the original.
After each iteration: By the previous iteration, A starts out as a permutation of the original array. Because we only modify A by swapping elements, it remains a permutation of the original at the end of this iteration.
To show that the output is sorted in decreasing order, we also use the loop invariant technique, but to the stronger claim that after iteration i, the subarray A[1 \dots i] is sorted in decreasing order and contains the i largest elements of A.
Before the loop starts: A[1 \dots 0] is empty (thus sorted) and certainly contains the 0 largest elements of A.
After each iteration: By the previous iteration, A[1 \dots i-1] starts sorted in decreasing order and containing the i-1 largest elements of A. So the ith largest element is the largest element in A[i \dots n], which is A[j]. We swap A[i] and A[j], so A[i] ends up the ith largest element. Thus A[1 \dots i] is sorted and has the i largest elements of A. ∎
It would not have worked to just prove that the output is
sorted in decreasing order, because it is actually not true that
if A[1 \dots i-1] is sorted in
decreasing order, then applying one iteration of the pseudocode
results in A[1 \dots i] being
sorted in decreasing order
. For example, if A = [9, 8, 7, 1, 2, 10], then it is
true that A[1 \dots 3] is sorted
in decreasing order. Applying one iteration of the pseudocode
results in A = [9, 8, 7, 10, 2,
1], and it is not true that A[1
\dots 4] is sorted in decreasing order. In other words,
although A[1 \dots i] being
sorted in decreasing order
is true, the implication above that
we would use to attempt a proof is false, so we needed to add the
fact that A[1 \dots i] contains
the i largest elements of A.
See Lecture 3 for an alternative proofs.
See Lecture 4.