From Visualization to Coding: Practicing Graphical Loop Invariants in CAFÉ 2.0

This talk 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 is 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 talk 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 talks also discusses an integrated learning tool we developed for supporting the Graphical Loop Invariant teaching and practice. Finally, the talk gives insight into how students seize the methodology and use the learning tools for supporting their learning phase.