Lecture Notes for Advanced Programming II

10 September 2002 - Invariants

1. loop invariants

   1. straight-line programs are easy to understand (relatively)

   2. programs with loops are harder to understand

      1. what's happening while it's looping

      2. when does it stop looping

   3. the trick - find something about the loop that's always true

      1. easier to verify something stays true

      2. always true - before, during, and after

   4. example - search for an element in a vector

   5. the invariant must be true before the loop executes

   6. it must be true after the guard executes

   7. it must be true at the end of the loop body

   8. it will be true after the loop exits

   9. the combination of the invariant and negated loop guard gives what we want

This page last modified on 17 September 2002.