CSC 240 LECTURE 9 CORRECTNESS OF ALGORITHMS
Consider the following algorithm:
M(m,n)
z←0
w←m
while w ≠ 0 do
z←z + n
w←w – 1 return(z)
What does it mean that an algorithm is correct? That it satisfies its specifications.
Specifications are often written using preconditions and postconditions.
A precondition is a statement (an assertion) involving the variables used in the algorithm.
It says that certain facts must be true before an execution of the algorithm begins.
It can describe which inputs are allowable.
A postcondition is also a statement about variables used in the algorithm. It says that certain facts must be true when an execution of the algorithm ends.
Often a postcondition describes the correct output (or possible correct outputs) for a given input.
We are also concerned about termination of an algorithm: it halts (provided the preconditions hold).
partial correctness:
if the preconditions hold, the algorithm is executed, and it eventually halts, then the postconditions hold.
termination:
if the preconditions hold, and the algorithm is executed, then
it eventually halts.
total correctness = partial correctness + termination
Algorithm M performs multiplication by repeated addition. It starts z at 0 and adds n to z a total of m times.
M(m,n)
z←0
w←m
while w ≠ 0 do
z←z + n
w←w – 1 return(z)
Precondition: m,n ∈Z Postcondition: z = m x n
n ∈Zand m ∈N
Is M correct with respect to these specifications?
NO. If m < 0, then M doesn’t halt.Example 1specifications for search of an array A for a value/key kPrecondition:The elements of A[1..n] and k are from the same domain. Postcondition:return an integer i such that 1 ≤ i ≤ length(A)and A[i] = k, if such an integer i exists; otherwise return 0. A and k must not be changed.Note: the specifications don’t say how the search is to be performed. It just gives the relationship between inputs and outputs.Consider the algorithm A[1] ← kreturn(1)It satisfies these specifications. So doesk ← A[1] return(1)Example 2specifications for binary search algorithmPrecondition: A[1..n] is sorted in non-decreasing order:∀ i ∈Z+. ∀ j ∈Z+. [(i < j ≤ length(A)) IMPLIES (A[i] ≤ A[j])]. Postcondition: return an integer i such that 1 ≤ i ≤ length(A) and A[i] = k, if such an integer i exists; otherwise return 0.A and k are not changed.If the precondition isn’t satisfied, an algorithm may return an incorrect answer, it may run forever, or it may perform an illegal operation such as dividing by 0.Example 3specifications for sorting an array APrecondition: the elements in A are from a totally ordered domain, i.e. comparable to one anotherPostcondition: the elements of A are in nondecreasing orderand the elements in A after the algorithm has executedare a permutation of the elements in A before the algorithm executed.Example 4specifications for merging two arrays A and B Preconditions:A and B are in nondecreasing orderThe elements in A and B are from a totally ordered domain Postconditions:C is in nondecreasing orderthe multiset of elements in C is equal to the union ofthe multiset of elements in A and the multiset of elements in B. A and B are unchanged.Proving Correctness of Recursive Algorithmsusually use induction Example 5MERGESORT(A,n) 1. if n > 1 then
2. m ← ⎣n/2⎦
3. U ← A[1..m]
4. V ← A[m+1..n]
5. MERGESORT(U,m) 6. MERGESORT(V,n-m) 7. A ← MERGE(U,V)
8. return
Proof of correctness, by induction:
For n ∈ N, let P(n) = “for all arrays A[1..n] with elements from a totally ordered domain,
if MERGESORT(A,n) is performed,
then it eventually halts, at which time A is sorted in nondecreasing order and the multiset of elements in A is unchanged”.
Let n ∈ N be arbitrary. Let A[1..n] be an arbitrary array with elements from a totally ordered domain.
Consider MERGESORT(A,n).
Base cases: n = 0,1.
The test on line 1 fails and A is unchanged.
Also note that A is sorted in non-decreasing order. By generalization, this holds for all arrays A[1..n]. Hence P(n) is true.
Induction cases: n > 1.
Suppose P(n’) is true for all natural numbers n’ < n.The test on line 1 succeeds and m = ⎣n/2⎦ from line 2.Then m, n-m < n.By the induction hypothesis,after MERGESORT(U,m) and MERGESORT(V,n-m) are performed,U and V are each sorted in nondecreasing orderthe multiset of elements in U is the multiset of elements in A[1..m],and the multiset of elements in V is the multiset of elements in A[m+1..n].Note that the union of the multiset of elements in U and V is the set of elements originally in A.It follows from the correctness of MERGE that,after A ← MERGE(U,V) is performed,the elements in A are sorted in nondecreasing order and the multiset of elements in A is the union ofthe multiset of elements in U and V.Hence the multiset of elements in A is unchanged.It follows by generalization that P(n) is true and, by induction, that ∀ n ∈ N. P(n) is true. Hence MERGESORT is correct.Proving Correctness of Iterative Algorithmstermination and partial correctness are often proved separately.Example 6MULTbyAdd(m,n)1. z ← 02. w ← m3. while w ≠ 0 do4. z ← z + n5. w ← w – 16. return(z)The hard part is dealing with loops.What can we say about the value of the variables immediately after the i’th iteration of the loop?w = m -i z = nx iConvention: immediately after the 0’th iterationis equivalent to immediately before the first iteration.We can prove these statements by induction on i:Let P(i) = “if the loop is executed at least i times, then, immediately after the i’th iteration w = m – i and z = n x i.LEMMA 1 Let m ∈Nand n ∈Z. For all i ∈N, P(i) is true. Proof:Let wi and zi denote the values of w and z immediately after the i’th iteration.Initially, w0 = m = m – 0 and z0 = 0 = n x 0, from lines 1 and 2, so P(0) is true.Let i ≥ 0 and assume P(i) is true.Then wi = m – i and zi = n x i.Assume the loop is executed at least i+1 times.From lines 4 and 5, zi+1 = zi + n = n x i + n = n x (i+1) and wi+1 = wi – 1 = m – i – 1 = m – (i+1). Hence P(i+1) is true.By induction, ∀i∈ N. P(i).COROLLARY 2 (Partial correctness) Let m ∈ N and n ∈ Z.If MULTbyAdd(m,n) is run and it halts, then, when it halts, z = n x m.Proof:Suppose the loop halts immediately after the i’th iteration. From the termination condition of the loop (line 3), wi = 0. By the lemma, wi = m – i and zi = n x i,so i = m and zi = n x m.Another proof of partial correctness:Combine w = m – i and z = n x i to get z = n x (m-w).This is nice because it doesn’t involve i.It is the same immediately after every iteration of the loop.A loop invariant is a predicate that is trueeach time a particular place in the loop is reached. Often, we consider the beginning/end of the loop, but, sometimes, it is easier to consider other places. If we don ‘t specify the location, we mean it is true at the beginning/end of every iteration of the loop.LEMMA 3 z = n x ( m – w ) is a loop invariant.Proof: Initially, from lines 1 and 2,z = 0 and w = m so n x ( m – w ) = 0 = z.Consider an arbitrary iteration of the loop.Let w’ and z’ denote the values of w and z at the beginningof the iteration andlet w” and z” denote the values of w and z at the end of the iteration.Suppose the claim is true at the beginning of the iteration. Then z’ = n x ( m – w’ ).From lines 4 and 5 of the code, w” = w’ – 1 and z” = z’ + n,so n x ( m – w” ) = n x ( m – (w’ – 1) ) = n x ( m – w’) + n = z’ + n = z”. Thus the claim is true at the end of the iteration.Hence, by induction, z = n x ( m – w ) after every iteration.COROLLARY 4 (Partial correctness) Let m ∈ N and n ∈ Z.If the algorithm is run and it halts, then, when it halts, z = n x m.Proof: From the termination condition of the loop (line 3), w = 0. By Lemma 3, z = n x ( m – w ) = n x m.TerminationProving termination is easy if no while loops, repeat until loops,or recursion, assuming any subprograms that are called terminate.For while loops and repeat until loops, to show termination, it suffices to show that some non-negative integral quantity decreases each time through the loop.MULTbyAdd(m,n)1. z ← 02. w ← m3. while w ≠0 do4. z ← z + n5. w ← w – 16. return(z)LEMMA 5 (Termination) If n ∈ Z, m ∈ N, and MULTbyAdd(m,n) is run, it eventually halts.Proof:Before the loop is executed, w is set to the natural number m. Each iteration of the loop w is decreased by 1,so it is a smaller natural number.Hence, w must eventually reach 0.This is the exit condition of the loop.Therefore, the loop terminates and the algorithm halts.Somewhat more formally:Suppose the loop doesn’t terminate.Let wi be the value of w immediately before the i’th iteration of the loop. From line 5, wi+1 = wi-1.Let Q(i) = “wi ∈ N”.Since w1 = m ∈N, Q(1) is true.Let i ≥ 1 be arbitrary and suppose Q(i) is true.Since the loop doesn’t terminate, wi ≠ 0. Thus wi ∈ Z+. Since wi+1 = wi -1, it follows that wi+1 ∈ N.Hence Q(i+1).By induction, ∀ i ∈ Z+. Q(i).Thus w1, w2 … is a sequence of natural numbers.By the well-ordering principle, the set of elements in this sequence has a smallest element, wi.But wi+1 < wi.This contradicts the definition of wi.Thus, the loop eventually terminates.Example 7MULTbyShift&Add(m,n) 1. w ← m2. y ← n3. z ← 04. while w ≠ 0 do5. if w mod 2 = 1 then z ← z + y6. w ← w div 2 %quotient when w is divided by 2 7. y ← 2 x y %or y ← y + y8. return(z)Note that division and multiplication by 2 are implemented using shift.Preconditions: m ∈ N, n ∈ Z Postconditions: z = n x mHow to come up with loop invariants?1. look at examples:m = 11, which is 1011 in base 2 n = 20, which is 10100 in base 2Let wi, yi and zi denote the values of w, y, and z immediately after the i’th iteration of the while loop.i wi0 1115 101 1 40 22 10 0 80 31 1 1 160 40 0 0 320 wi = ⎣ m / 2i ⎦yi = n 2i zi = ?2. use your understanding 10100×1011 ————10100 1010000000 10100 ————- 11011100zi020 = n = 1 y060 = 2n + n = 1y1 + 1 y060 = 2n + n = 0 y2 + 1 y1 + 1 y0220 = 8n + 2n + n = 1 y3 + 0 y2 + 1 y1 + 1 y0how the algorithm is supposed to workbinary wi mod 2 yi 1011 1 20ofLet m[k-1] … m[1] m[0] denote the binary representation of m, so m = ∑ {m[a] 2a | 0 ≤ a ≤ k-1}where m[a] ∈ {0,1} for 0 ≤ a ≤ k-1.For example, m = 1110 = 10112, k = 4, m[3] = 1, m[2] = 0, m[1] = 1, m[0] = 1.wi is obtained from m by deleting the i least significant bits wi = ∑ {m[a] 2^{a-i} | i ≤ a ≤ k-1}wi 2i = ∑ {m[a] 2a | i ≤ a ≤ k-1}Since m = ∑ {m[a] 2a | 0 ≤ a ≤ k-1} andwi+1 2^{i+1} = ∑ {m[a] 2a | i+1 ≤ a ≤ k-1} it follows thatm – wi+1 2^{i+1} = ∑ {m[a] 2a | 0 ≤ a ≤ i}.The least significant bit of wi is m[i], so wi mod 2 = m[i].Initially, y = n. Each time through the loop, the value of y is doubled. Thus yi = n 2i.z0 = 0 from its initialization on line 3zi+1 = zi + m[i] yi since z ← z + y if w mod 2 = 1= zi + m[i] n 2iusing repeated substitutionzi+1 = m[0] n 20 + m[1] n 21 + … + m[i] n 2i= n ∑ {m[a]2a | 0 ≤ a ≤ i } = n ( m – wi+1 2^{i+1} )= nm – wi+1 x yi+1MULTbyShift&Add(m,n)1. w ← m2. y ← n3. z ← 04. while w ≠ 0 do5. if w mod 2 = 1 then z ← z + y6. w ← w div 2 %quotient when w is divided by 2 7. y ← 2 x y %or y ← y + y8. return(z)LEMMA 6 If m ∈ N and n ∈ Z, then z = n x m – w x y and w ∈ N are loop invariants.Proof:Note that m and n aren’t changed by the algorithm, since there are no assignments to m and n.Initially, z = 0, w = m ∈ N and y = n by lines 1,2, and 3 so n x m – w x y = 0 = z.Consider an arbitrary iteration of the loop.Let w’,y’ and z’ denote the values of w, y, and z at the beginningof the iteration andlet w”, y”, and z” denote the values of w, y, and z at the end of the iteration.Suppose the claim is true at the beginning of the iteration. Then z’ = n x m -w’ x y’ and w’ ∈ N.From line 7 of the code y” = 2y’.Case 1: w’ is odd.Then, from lines 5 and 6 in the code, z” = z’ + y’ and w” = (w’-1)/2 ∈ N, so n x m – w” x y” = n x m – (w’-1)/2 x 2y’= n x m – (w’-1) x y’ = n x m – w’ x y’ + y’= z’ + y’ = z”.Case 2: w’ is even.Then, from lines 5 and 6 in the code, z” = z’ and w” = w’/2 ∈ N, so n x m – w” x y” = n x m – w’/2 x 2y’= n x m – w’ x y’ = z’= z”.Since w’ is either even or odd, the claim is true at the end of the iteration. Hence, by induction, z = n x m – w x y is a loop invariant.Where do we use the assumption that m ∈ N? In the statement w’ is either even or odd.LEMMA 6 (corrected) If m ∈ N and n ∈ Z, then and z = n x m – w x y are loop invariants.COROLLARY 7 (partial correctness) Let m ∈ N and n ∈ Z.If MULTbyShift&Add(m,n) is run and it halts, then, when it halts, z = n x m.Proof:Assume MULTbyShift&Add(m,n) is run and it halts.From the termination condition of the loop (while w ≠ 0 do) w= 0 when the loop terminates.By Lemma 6, z = n x m – w x y. Hence z = n x m.Q: Why does MULTbyShift&Add(m,n) terminate? w gets smaller every iteration, provided w ≥ 1.
Reviews
There are no reviews yet.