The development, specification, and use of a loop invariant are useful and underutilized tools in writing code to solve a problem or implement an algorithm. Invariants are especially useful in introductory courses (CS1 and CS2) but are usually avoided because of the mathematical notation associated with them and because most textbooks have brief, if any, coverage of them. Our intent in this paper is provide several motivating examples of the use of pictures as loop invariants and to provide pointers to literature that more fully explores and develops the ideas of using loop invariants in specifying and developing programs.
Owen L. Astrachan