Teaching Design by Contract Using Snap!

Marieke Huisman; Raúl E. Monti

doi:10.1007/978-3-031-08166-8_12

Teaching Design by Contract Using Snap!

Marieke Huisman, Raúl E. Monti^*

^*Corresponding author for this work

Formal Methods and Tools

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

33 Downloads (Pure)

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 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 also make this as intuitive as possible. Finally, we outline how program verification in Snap! could be introduced to high school students in a classroom situation.

Original language	English
Title of host publication	The Logic of Software
Subtitle of host publication	A Tasting Menu of Formal Methods
Editors	Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Einar Broch Johnsen
Publisher	Springer
Pages	243–263
Number of pages	21
Edition	1
ISBN (Electronic)	978-3-031-08166-8
ISBN (Print)	978-3-031-08165-1
DOIs	https://doi.org/10.1007/978-3-031-08166-8_12
Publication status	Published - 2022

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	13360
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Keywords

2024 OA procedure

Access to Document

10.1007/978-3-031-08166-8_12

ArticleFinal published version, 3.66 MBLicence: Taverne

1 Conference contribution
1 Working paper

Teaching Design by Contract using Snap!
Huisman, M. & Monti, R. E., 8 Jul 2021, Proceedings - 2021 3rd International Workshop on Software Engineering Education for the Next Generation, SEENG 2021. Piscataway, NJ: IEEE, p. 1-5 5 p. 9474640
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Open Access
File
2 Citations (Scopus)

82 Downloads (Pure)
Teaching Design by Contract using Snap!
Huisman, M. & Monti, R. E., 12 Jul 2021, ArXiv.org.
Research output: Working paper

Open Access
File
95 Downloads (Pure)

Cite this

@inbook{53f610bba8ae4d65ad379f95e99a30b4,

title = "Teaching Design by Contract Using Snap!",

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 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 also make this as intuitive as possible. Finally, we outline how program verification in Snap! could be introduced to high school students in a classroom situation.",

keywords = "2024 OA procedure",

author = "Marieke Huisman and Monti, {Ra{\'u}l E.}",

year = "2022",

doi = "10.1007/978-3-031-08166-8_12",

language = "English",

isbn = "978-3-031-08165-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "243–263",

editor = "Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Johnsen, {Einar Broch}",

booktitle = "The Logic of Software",

address = "Germany",

edition = "1",

}

Teaching Design by Contract Using Snap! / Huisman, Marieke; Monti, Raúl E.
The Logic of Software: A Tasting Menu of Formal Methods. ed. / Wolfgang Ahrendt; Bernhard Beckert; Richard Bubel; Einar Broch Johnsen. 1. ed. Springer, 2022. p. 243–263 (Lecture Notes in Computer Science; Vol. 13360).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

TY - CHAP

T1 - Teaching Design by Contract Using Snap!

AU - Huisman, Marieke

AU - Monti, Raúl E.

PY - 2022

Y1 - 2022

N2 - 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 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 also make this as intuitive as possible. Finally, we outline how program verification in Snap! could be introduced to high school students in a classroom situation.

AB - 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 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 also make this as intuitive as possible. Finally, we outline how program verification in Snap! could be introduced to high school students in a classroom situation.

KW - 2024 OA procedure

U2 - 10.1007/978-3-031-08166-8_12

DO - 10.1007/978-3-031-08166-8_12

M3 - Chapter

SN - 978-3-031-08165-1

T3 - Lecture Notes in Computer Science

SP - 243

EP - 263

BT - The Logic of Software

A2 - Ahrendt, Wolfgang

A2 - Beckert, Bernhard

A2 - Bubel, Richard

A2 - Johnsen, Einar Broch

PB - Springer

ER -