Graphical Loop Invariant Based Programming

This paper focuses on a programming methodology relying
on an informal and graphical version of the Loop 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 writ-
ing 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 sup-
porting 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.