A note on a standard strategy for developing loop invariants and loops

AbstractA by-now-standard strategy for developing a loop invariant and loop was developed in [1] and explained in [2]. Nevertheless, its use still poses problems for some. The purpose of this paper is to provide further explanation. Two problems are solved that, without this further explanation, seem difficult