SUNY Geneseo Department of Computer Science

Correctness of Insertion Sort

Return to List of Lectures

Misc

Problem Set 9 extended 'til Monday Mar. 6

Questions?

Proofs about loop invariants always induction

• If loop invariant holds in one iteration, then it holds in next

Insertion Sort

Prove that insertion sort leaves A in ascending order

    for ( i = 1; i < A.length; i++ ) {
        for ( j = i; j > 0 && A[j] < A[j-1]; j-- ) {
            k = A[j-1];
            A[j-1] = A[j];
            A[j] = k;
        }
    }

• Main (i) loop invariant: A[0..i-1] is in ascending order at beginning of loop
• Step 1: prove that "i" loop exits
  • Each iteration reduces "distance" between i and A.length
    • i.e., A.length - i gets smaller by 1, and the loop exits when this number is 0
• Step 2: prove that "j" loop exits
  • Each iteration reduces distance between j and 0
• Step 3: Prove that loop invariant holds for inner loop
  • Invariant: A[j] through A[i] are in ascending order at beginning of inner loop
  • Base case: when loop starts, j = i, A[j..i] only has 1 element, must be in order
  • Induction (mini-assignment)
    • "If invariant holds at start of some iteration, does it hold at start of next?"
    • i.e., assume invariant holds at start of iteration k-1, show that it holds at start of iteration k
    • i.e., assume at start of k-1 iteration, A[j..i] in ascending order
    • What will j be at start of next iteration?
      • j-1
      • i.e., show that at end of this iteration, A[j-1..i] in ascending order
    • Each iteration A[j-1] switches with A[j] if A[j] was less, i.e., would not be ascending order after j decreased by 1 (could prove switch correct too)
      • And original A[j-1] is less than A[j+1] by main loop invariant

• Step 4: Prove invariant for i loop
  • i.e., A[0..i-1] is in ascending order at beginning of loop
  • When i = 1, A[0..i-1] = A[0..0], 1 element, vacuously ascending
  • If at the start of some iteration, A[0..i-1] ascending, then...
    • When inner loop exits, A[j..i] ascending
      • j = 0: Inner loop invariant implies A[j=0..i] ascending
      • A[j-1] <= A[j]: outer loop invariant says A[0..j-1] ascending (since i-1 is at least j-1),
        • and A[j-1] <= A[j],
        • and A[j..i] ascending
        • Collectively imply A[0..i] ascending
    • Therefore A[0..i] ascending at the end of that iteration
  • ... Therefore at start of next iteration, A[0..i-1] ascending even though i has changed, increased by 1

Next

How fast are these sorting algorithms?

Read section 9.1 through 9.1.3 (pages 275 through 281)