Loop Invariants, Part 2

Return to List of Lectures

Previous Lecture

• Misc
  • Colloquium writeups now are nice, but I’ll accept them any time ’til end of semester
• Questions?
• Correctness and Loop Invariants
  • Inner loop from insertion sort
    • Invariant might be “for all k such that i ≤ k < j, A[k] > key”
      • This is a loop invariant, but it turns out not to be useful for proving overall result that A[1..j] is sorted
    • So look for another invariant...
      
  • Fast multiplication
    • Idea:
      • xy = 2 (x/2) y = (x/2) (2y) if x is even
      • xy = (x-1) y + y if x is odd
      • (In base 2, multiplication and division by 2 are easy, as multiplication and division by 10 are in base 10)
        • 102 * 10 = 1020
        • 120 / 10 = 12
          

          times( x, y )            // initial x, y are x0, y0
              product = 0
              while x > 0          // inv: product + xy = x0y0
                  if x is even
                      x = x/2
                      y = 2 * y
                  else             // x is odd
                      x = x-1
                      product = product + y
                  end of if
              end of while
              return product

• Next
  • Recursion
  • Watch “Recursion” video at https://www.youtube.com/watch?v=t4MSwiqfLaY

Next Lecture