Checklist for loops
Show that P is true before the execution of a loop begins
Show that P ? ?BB ? R i.e. when the loop terminates the desired result is true.
Show that {P ? Bi} Si {P} 1<=i<=n i.e. execution of each guarded command terminates with P true so that P is an invariant of the loop.
Show that P ? BB ? (t ɬ) so that the bound function i.e. “the amount of work yet to be done” is bounded from below as long as the loop has not terminated.
Show that {P ? Bi} t1 :=t;Si; {t<t1} for 1 <=i<=n so that each loop iteration is guaranteed to decrease the bound function. In general t can only provide an upper bound on the number of iterations to be performed. Hence, it is called the bound function or the variant function.