Proof Plan
-
Generate the invariant INV
and prove the body, that is,
show that INV exhibits the properties of an
invariant for this particular while loop body.
-
Push INV back through the multiassignment and
show that PRE implies the transformed predicate.
-
Push INV forward to the end of the program and
show that the transformed predicate implies POST.