Pictures as invariants

The development, specication, 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 in-troductory courses (CS1 and CS2) but are usu-ally avoided because of the mathematical nota-tion associated with them and because most text-books have brief, if any, coverage of them. Our intent in this paper is provide several motivating examples of the use of pictures as loop invari-ants and to provide pointers to literature that more fully explores and develops the ideas of us-ing loop invariants in specifying and developing programs.