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.

Recursion:
Recursion is another algorithm design technique, closely related to iteration, but more powerful. Using recursion, we solve a problem with a given input, by solving the same problem with" a part of the input, and constructing a solution to the original problem from the solution to the partial input.

a loop variant, then it is true at four important points in the algorithm
(i) at the start of the loop (just before the loop).
(ii) at the start of each iteration (before loop body)
(iii) at the end of each iteration (after loop body).
(iv) at the end of the loop (just after the loop).

Let P (p, c) = p - c. Then
P (p, c) [p, c := p + 1, c + 1]
= p - c [p, c := p + 1, c + 1]
= (p + 1)-(c + 1)
= p-c
= p(P, c)
Since (p - c) [p, c := p + 1, c + 1] = p - c, p - c is an invariant of the assignment p, c := p + 1, c + 1.

(I) In iteration, the loop body is repeatedly executed as long as the loop condition is true. Each time the loop body is executed, the variables are updated.
(ii) However, there is also a property of the variables which remains unchanged by the execution of the loop body.
(iii) This unchanging property is called the loop invariant. Loop invariant is the key to construct and to reason about iterative algorithms.