Example 1: Proof Plan
OUTLINE OF PROOF
Generate a loop invariant INV, and show that INV is invariant for the loop
Push the INV back to the beginning of the program,
and show that the 'PRE' spec implies the transformed INV
Push INV forward to the end of the program and show that
the transformed INV implies the 'POST' spec.