Graphical Loop Invariant Based Programming

This paper focuses on a programming methodology relying on an informal and graphical version of the \invariant for building the code. This methodology is applied in the context of a CS1 course in which students are exposed to several C programming language concepts and algorithmic aspects. The key point in the course is thus to imagine a problem resolution strategy (the Graphical Loop Invariant) prior to writing the code (that becomes, then, reasonably easy once relying on the Graphical Loop Invariant). This paper exposes the rules for building a sound and accurate Graphical Loop Invariant as well as the programming methodology. As such, our programming methodology might be seen as a first step towards considering formal methods in programming courses without making any assumption on students mathematical background as it does not require to manipulate any mathematical notations. The paper also introduces an integrated learning tool we developed for supporting the Graphical Loop Invariant teaching and practice. Finally, the paper gives preliminary insight into how students seize the methodology and use the learning tools for supporting their learning phase.