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.