Developing Loop Invariants Strategy

A by-now-standard strategy for developing a loop invariant and loop is explained in this paper. Two problems are solved that, without this explanation, seem difficult.