SUNY Geneseo Department of Computer Science

Loop Invariants

Return to List of Lectures

Misc

Lab 5 and Problem Set 8 due tomorrow

Questions?

Loop Invariants

Section 8.1

• Definition
  • Loop invariants are things that don't change as loop iterates
• Examples of designing code using loop invariants
  • Binary search
    • How algorithm follows from loop invariant
  • GCD algorithm

Example - sorting arrays

• Consider sorting by stepping an index, i, through an array, A, while maintaining the loop invariant "elements 0 through i-1 of A are in ascending order" (this holds at the beginning of each iteration)
• One element by itself is always sorted
  • So initialization can be

            i = 1

• Code ideas
  • When i changes, i > 1, check if A[i] > A[i-1], if not switch

            while A[i] not in right spot
                switch A[i] with previous element

• Maintains loop invariant
• Changing i

            i = i + 1

• Exit
  • i >= A.length
• Or continuation condition
  • i < A.length
• "Runnable" code

        for ( i = 1; i < A.length; i = i + 1 ) {
            // i is about to increase by one, have to prepare
            // by making sure loop invariant will still hold.
            // Do this by shifting A[i] down through A[0...i-1]
            // to put A[0 ... i] into order.
            for ( j = i; j > 0; j-- ) {
                if ( A[j] < A[j-1] ) {
                    k = A[j-1];
                    A[j-1] = A[j];
                    A[j] = k;
                }
                else {
                    break;
                }
            }
        }

• Illustrates algorithm design from loop invariant
  • Start with problem (sorting)
  • Vague idea (step i through A, keeping A[0..i-1] sorted)
  • Loop invariant from vague idea
  • Invariant justifies everything in loop
    • Initialization
    • Change / restore invariant pattern
    • Termination / loop's correctness

Hand out Lab 6

Next

Using loop invariants (among other things) to prove loops correct

Read section 8.2 up through 8.2.3 (i.e., pages 253 bottom through 264 middle)