COMP3600/6466 – Algorithms
Correctness [CLRS sec. 2.1]
Hanna Kurniawati
https://cs.anu.edu.au/courses/comp3600/ comp_3600_6466@anu.edu.au
Recall Algorithm Definition
• An algorithm is a well-defined computational procedure (i.e., computational steps) that transforms input to output for solving a well-specified computational problem
• Well-defined: Can specify when & where the procedure works and when it is not
• Correctness
• Space & time requirements
Correctness
• Not sufficient to just look correct. Needs proof.
• Proving correctness of an algorithm is not easy,
and as per our last week lecture, in this class
we’ll cover this topic very briefly
• Proving correctness of incremental algorithm using loop invariant concept –akin to proof by induction
• Loop invariant: The condition that is true at the beginning and end of each iteration
Correctness via Loop Invariant
• First, state the statement we want to proof as a loop invariant
• Then, show the following three things:
• Initialization: The statement we want to proof is correct
prior to the first iteration of the loop
• Maintenance: If the statement is correct before an iteration of the loop, it remains correct before the next iteration
• Termination: When the loop terminates, the result helps show correctness of the statement
Recall Proof by Induction
• Suppose we want to proof a statement S(n)
• Proof by induction consists of:
• Basis step: Show the statement is true for a base case
• Inductive hypothesis: Assume S(n) is true
• Inductive step: Show that for all positive integer n, if
S(n) is true, then S(n+1) is true
• Loop invariant resembles proof by induction:
• Initialization – Base case
• Maintenance – Inductive step
• Though, in loop invariant, we need need to show termination rather than applying inductive step infinitely
Example: Insertion Sort
InsertionSort(A)
1
for j = 2 to A.length
2
Key = A[j]
3
i = j-1
4
While i > 0 and A[i] > key
5
A[i+1] = A[i]
6
i = i-1
7
A[i+1] = key
• Show that Insertion Sort outputs a sorted array
Example: Insertion Sort
• Loop invariant statement: At the start of each iteration of the outer-loop, the subarray 𝐴[1, … , 𝑗 − 1] consists of elements in the input array 𝐴 1,…,𝑗 − 1 but in sorted order
• To proof the above loop invariant, we show:
• Initialization: When 𝑗 = 2, the subarray only consists of 1 element: 𝐴[1] and this element is the same as the original value element. Obviously, the loop invariant holds (trivially).
• Maintenance: Lines 3-6 move 𝐴 𝑗 − 1 , 𝐴[𝑗 − 2], … by 1 position totherightuntiltherightpositionfor𝐴𝑗 isfound,atwhichpoint (line 7), it inserts the value of 𝐴 𝑗 . The subarray 𝐴[1, … , 𝑗] then consists of the elements originally in the input array 𝐴[1, … , 𝑗] but in sorted order. Incrementing 𝑗 for the next iteration preserves the loop invariant.
Example: Insertion Sort
• Termination: The condition causing termination is 𝑗 > 𝑛. Since each loop increases 𝑗 by one, at termination, we must have 𝑗 = 𝑛 + 1. Substituting 𝑛 + 1 for 𝑗 in the loop invariant statement, we have:
At the start of each iteration of the outer-loop, the subarray 𝐴[1, … , 𝑛] consists of elements in the input array𝐴1,…,𝑛 butinsortedorder
The above means the entire array is sorted. And therefore, the algorithm is correct.
Next: Recurrence Analysis