1. Establish the loop invariant at the start of the loop.
2. The loop body should so update the variables as to progress toward the end, and maintain the loop invariant, at the same time.
3. When the loop ends, the termination condition and the loop invariant should establish the input – output relation.