Loop invariants, exploration of regularities, and mathematical games

Loop invariants are assertions of regularities that characterize the loop components of algorithms. They are fundamental components of computerprograms verification, but their relevance goes beyond verification-they can be significantly utilized for algorithm design and analysis. Unfortunately, they are only modestly introduced in the teaching of programming and algorithms. One reason for this is an unjustified notion that loop invariants are 'tied to formality', hard to illustrate, and difficult to comprehend. In this paper a novel approach is presented for illustrating on a rather intuitive level the significance of loop invariants. The illustration is based on mathematical games, which are attractive examples that require the exploration of regularities via problemsolving heuristics. Throughout the paper students' application of heuristics is described and emphasis is placed on the links between loop invariants, heuristic search activities, recognition of regularities and design and analysis of algorithms.