Reasoning about loops

Two Common Ways to Reason About Loops:

1. loop tracing - tracing through a loop based on some input
2. loop invariant - captures what the loop does not do, i.e., what it leaves unchanged over any single execution of the loop body (and hence over the entire execution of the loop)

Loop Invariant

• Invariant means unchanged
• The person who writes the loop, also writes the loop invariant which describes what remains unchanged
• Permits understanding what the loop does without having to understand (at the same time) how it does it.
• We can reason about the loop's effect on the larger program without hand tracing each loop iteration.
   
• Loop Invariant Parts:
  1. material objects lists
     • up to four lists (i.e., alters, consumes, preserves, produces), each list (if not empty) contains the names of objects involved in the loop
     • one list of objects per usage mode (i.e., alters, consumes, preserves, produces), as though the loop were an operation and these objects were the formal parameters to it
     • the mode indicates what happens to each object's value over the course of a single iteration of the loop body, not over the entire execution of the loop
  2. invariant property
     • an assertion about what the loop body does not do to the state of the program when the loop body is executed
     • a Boolean-valued expression which involves only the material objects
     • the material objects can appear with and without the '#' prefix
     • the '#' prefix means the value of the object immediately before the loop is encountered
        
• Correctness of the Loop Invariant:
  1. The invariant property must hold in the state just before the first test of the while (or other loop) condition.
  2. The invariant property must hold in the state at the very end of the sequence of statements in the loop body.
  3. All objects mentioned in the material objects lists must be involved in the loop condition, or the loop body, or both; and only those objects must be so involved.
      
• What is True at Loop Termination:
  1. The loop invariant holds.
  2. The while (or other loop) condition itself does not hold in this state.
  3. All objects in the program that are not listed as material objects have the same values as they had just before the first test of the while condition.