Teaching Design by Contract using Snap!

Marieke Huisman, Raul E. Monti

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

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 verification of Snap! programs. Special attention is given to the error messaging, to make this as intuitive as possible.

Original languageEnglish
Title of host publicationProceedings - 2021 3rd International Workshop on Software Engineering Education for the Next Generation, SEENG 2021
Place of PublicationPiscataway, NJ
PublisherIEEE
Pages1-5
Number of pages5
ISBN (Electronic)978-1-6654-3196-5
ISBN (Print)978-1-6654-3197-2
DOIs
Publication statusPublished - May 2021
Event3rd International Workshop on Software Engineering Education for the Next Generation, SEENG 2021 - Virtual, Online
Duration: 24 May 2021 → …

Conference

Conference3rd International Workshop on Software Engineering Education for the Next Generation, SEENG 2021
CityVirtual, Online
Period24/05/21 → …

Keywords

  • education
  • software
  • verification

Fingerprint

Dive into the research topics of 'Teaching Design by Contract using Snap!'. Together they form a unique fingerprint.

Cite this