Example 1: Proof Plan

OUTLINE OF PROOF

  1. Generate a loop invariant INV, and show that INV is invariant for the loop

  2. Push the INV back to the beginning of the program, and show that the 'PRE' spec implies the transformed INV

  3. Push INV forward to the end of the program and show that the transformed INV implies the 'POST' spec.