💻 computer science

CAFÉ, an automated feedback tool to approach Formal Methods

This paper presents CAFÉ, an automated feedback platform that scaffolds computer science students' transition to formal methods by guiding them to design Graphical Loop Invariants before coding, thereby providing personalized feedback on both their diagrammatic reasoning and final implementation.

Original authors: Géraldine Brieven, Ayman Labrahimi Kasdaoui, Benoit Donnet

Published 2026-07-07

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Géraldine Brieven, Ayman Labrahimi Kasdaoui, Benoit Donnet

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are teaching someone how to build a house. Most programming classes start by handing the student a hammer and a saw, saying, "Just start nailing boards together and see what happens." This is operational thinking: focusing on the immediate steps.

The paper introduces a new tool called CAF´E (Computer-Assisted Formal Education) that tries to teach students a different way: structural thinking. Instead of just hammering away, CAF´E asks students to first draw a detailed blueprint that explains why the house will stand up before they ever pick up a tool.

Here is a breakdown of the paper's ideas using everyday analogies:

1. The Problem: The "Hammer First" Approach

In computer science, a very common task is the loop (a set of instructions that repeats, like a conveyor belt). Beginners often struggle with loops because they focus on the next step rather than the whole picture. They try to code the loop without understanding the rules that keep it from running forever or crashing.

2. The Solution: The "Blueprint" (GLI)

The authors developed a method called GLIBP (Graphical Loop Invariant Based Programming).

The Analogy: Imagine a loop as a long line of people waiting to get their tickets checked.
The GLI (Graphical Loop Invariant): This is a visual diagram (a "blueprint") that students must draw. It doesn't just show the line; it shows a "dividing line" that moves down the queue.
- To the left of the line: Everyone has been checked (the "Done" zone).
- To the right of the line: Everyone is waiting to be checked (the "To Do" zone).
- The Rule: The diagram must show a rule that stays true no matter where the dividing line is. For example, "Everyone to the left has a valid ticket."

This forces the student to think about the state of the system (the whole line) rather than just the action (checking one person).

3. The Tool: CAF´E (The Automated Tutor)

CAF´E is a website that acts like a strict but helpful tutor. It doesn't just check if the final code works; it checks the student's "blueprint" (the GLI).

How it works:
- Students are given a problem (e.g., "Find the biggest number in a list").
- They must fill in a "fill-in-the-blank" version of the blueprint. Some boxes are free-for-all (write your own variable), while others are "constrained" (pick from a list of correct terms).
- The Magic: The system automatically checks if the student's blueprint makes sense.
  - Example: If the student writes that the "Done" zone starts at number 5, but the list only has 3 numbers, the system immediately says, "Wait, that's impossible!" and explains why.
- Once the blueprint is correct, the student writes the actual code. The system checks if the code matches the blueprint.

4. Why This Matters (The Results)

The paper claims that this approach helps students transition from "just coding" to "thinking like a mathematician" (Formal Methods).

The Evidence: The authors ran a study with students in a second-year course. They found a strong link: students who were good at drawing the "blueprints" (GLIs) were also very good at writing the formal mathematical rules (Formal Loop Invariants) later on.
The Metaphor: It's like teaching a driver to look at the road map and understand traffic laws before they are allowed to turn the key in the ignition. The paper suggests this prevents them from crashing later when the roads get more complex.

5. The Demo

The paper concludes by showing how the tool works for two types of people:

The Student: They log in, see a puzzle, fill in the boxes on their diagram, get instant feedback (like a "check engine" light that tells you exactly what's wrong), and try again.
The Teacher: They use a backend system to create new puzzles and define the "correct" blueprint rules, essentially designing the riddles for the students to solve.

In summary: CAF´E is a learning platform that forces computer science students to draw a visual "map" of their logic before they write a single line of code. By automating feedback on these maps, it helps students learn to build programs that are correct by design, not just by luck.

Technical Summary: CAF´E – An Automated Feedback Tool for Formal Methods in CS1

Problem Statement
The paper addresses the persistent challenge in computer science education of helping novice programmers transition from operational thinking (focusing on step-by-step execution) to structural thinking (focusing on properties and relationships). This shift is critical for mastering Formal Methods (FM) and writing correct programs, particularly regarding loop construction. While Formal Methods are increasingly adopted in industry, students often struggle with the abstract nature of loop invariants and assertions. Existing educational tools either lack support for graphical representations of invariants or fail to provide automated feedback on these representations, leaving students without immediate guidance on the structural correctness of their solutions.

Methodology: Graphical Loop Invariant Based Programming (GLIBP)
The authors propose and implement a learning platform called CAF´E (Computer-Aided Feedback Environment) to scaffold the learning of Formal Methods within an introductory programming (CS1) course. The core methodology is Graphical Loop Invariant Based Programming (GLIBP), which is grounded in Hoare's logic and Dijkstra's programming methodology.

The Graphical Loop Invariant (GLI): Instead of requiring students to write formal logical assertions immediately, the approach uses an informal, diagrammatic representation called a GLI. A GLI visualizes the objects being iterated over (e.g., arrays), the variables involved, their domains, and the relationships that must hold across iterations. It includes a "General State" that can be instantiated into "Initial" and "Final" states.
The CAF´E Platform: CAF´E operationalizes GLIBP by requiring students to solve loop-based problems in two stages:
- Fill-in-the-Blank GLI: Students complete a diagrammatic template containing "boxes." These boxes are either constrained (selecting from a predefined list of symbols) or free (entering expressions).
- Code Derivation: Based on the completed GLI, students write the corresponding C code, including variable initialization, loop guards, loop bodies, and a loop variant function to prove termination.
Automated Feedback Mechanism: To enable automation, the GLI is formalized via a metamodel and a configuration file. The system performs:
- Syntactic and Semantic Checks: Free boxes are validated against domains or dependency relationships with other boxes (e.g., ensuring a bound is boxB + 1). Constrained boxes are checked against expected symbol IDs.
- Consistency Checks: The system verifies the alignment between the GLI states (Initial, Final, General) and the submitted code, as well as the correctness of the loop variant function.
- Feedback Generation: Students receive personalized feedback identifying specific errors (e.g., LPM_boundVal for incorrect bounds, LPM_notConsec for non-consecutive values) before resubmitting.

Key Contributions

Development of CAF´E: A novel interactive online platform that uniquely combines the practice of structural thinking (via GLIs) with automated feedback on both the invariant diagram and the resulting code.
Formalization of GLIs for Automation: The authors define a rigorous metamodel that translates informal diagrammatic reasoning into checkable rules, allowing for the automated detection of common student misconceptions in loop invariants.
Integration into CS1 Curriculum: The tool is successfully deployed in a CS1 course using C, where it serves as a primary vehicle for introducing loop invariants before students encounter functions or formal specifications.
Proof-of-Concept for Formal Verification: The authors have developed a prototype that automatically translates GLIs and C code snippets into the Dafny language for formal verification, bridging the gap between introductory exercises and advanced FM.

Results and Evidence
The paper presents empirical evidence from the authors' CS1 and CS2 courses:

Correlation with Formal Specifications: In the CS2 course, a statistically significant positive correlation ( $r=0.63, p=0.00$ ) was observed between students' grades in drawing GLIs and their ability to write corresponding Formal Loop Invariants (FLIs). This suggests that the structural thinking fostered by GLIBP transfers effectively to formal specification tasks.
Educational Impact: The tool supports a "scaffolding" approach where students practice loop-based problems through three specific challenges (e.g., computing products of non-zero digits, compressing arrays). The automated feedback loop allows students to refine their structural understanding iteratively before final grading.

Significance and Claims
The paper claims that CAF´E is significant because it lowers the barrier to entry for Formal Methods by making the abstract concept of loop invariants accessible through visual, diagrammatic reasoning. By automating feedback on the structure of the solution (the GLI) rather than just the output (the code), the tool guides students to develop the "structural thinking" mindset required for writing correct programs.

The authors position CAF´E not as a replacement for formal logic but as a preparatory scaffold. They modestly claim that the tool serves as a valuable resource for educators aiming to introduce FM concepts early and for students struggling with the role of assertions. The work is presented as a step toward broader adoption of invariant-based programming, with the authors expressing openness to collaboration to extend the automated feedback features to other course contexts and formal verification tools.