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.