Teaching Design by Contract using Snap!
Marieke Huisman, Ra\'ul E. Monti

TL;DR
This paper introduces a visual program verification approach for Snap!, a high school programming language, making formal verification accessible through visual specifications and intuitive error messaging.
Contribution
It develops a novel, visually integrated specification and verification framework for Snap!, broadening access to formal methods for non-expert users.
Findings
Support for static and dynamic verification in Snap!
Visual specification constructs enhance understandability
Improved error messaging aids debugging
Abstract
With the progress in deductive program verification research, new tools and techniques have become available to support design-by-contract reasoning about non-trivial programs written in widely-used programming languages. However, deductive program verification remains an activity for experts, with ample experience in programming, specification and verification. We would like to change this situation, by developing program verification techniques that are available to a larger audience. In this paper, we present how we developed prototypal program verification support for Snap!. Snap! is a visual programming language, aiming in particular at high school students. We added specification language constructs in a similar visual style, designed to make the intended semantics clear from the look and feel of the specification constructs. We provide support both for static and dynamic…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Engineering Research · Software Engineering Techniques and Practices · Teaching and Learning Programming
