Transition Induction
lTo prove that an assertion
(e.g. a loop invariant) is true whenever
the program reaches the point to which the
assertion is attached:
¥Basis: Show that the
assertion is true the first time
¥Induction: Show that
if the assertion is true the current time (unprimed
variables), then it is true the next time (primed
variables), provided there is a next time.