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.