A Tool for Describing and Checking Natural Semantics Definitions of Programming Languages
Research output: Contribution to journal › Conference article › Research › peer-review
Standard
A Tool for Describing and Checking Natural Semantics Definitions of Programming Languages. / Saioc, Georgian Vlad; Hüttel, Hans.
In: Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol. 369, 2022, p. 51-66.Research output: Contribution to journal › Conference article › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - A Tool for Describing and Checking Natural Semantics Definitions of Programming Languages
AU - Saioc, Georgian Vlad
AU - Hüttel, Hans
N1 - Publisher Copyright: © 2022 Open Publishing Association. All rights reserved.
PY - 2022
Y1 - 2022
N2 - Many universities have courses and projects revolving around compiler or interpreter implementation as part of their degree programmes in computer science. In such teaching activities, tool support can be highly beneficial. While there are already several tools for assisting with development of the front end of compilers, tool support tapers off towards the back end, or requires more background experience than is expected of undergraduate students. Structural operational semantics is a useful and mathematically simple formalism for specifying the behaviour of programs and a specification lends itself well to implementation; in particular big-step or natural semantics is often a useful and simple approach. However, many students struggle with learning the notation and often come up with ill-defined and meaningless attempts at defining a structural operational semantics. A survey shows that students working on programming language projects feel that tool support is lacking and would be useful. Many of these problems encountered when developing a semantic definition are similar to problems encountered in programming, in particular ones that are essentially the result of type errors. We present a pedagogical metalanguage based on natural semantics, and its implementation, as an attempt to marry two notions: a syntax similar to textbook notation for natural semantics on the one hand, and automatic verification of some correctness properties on the other by means of a strong type discipline. The metalanguage and the tool provide the facilities for writing and executing specifications as a form of programming. The user can check that the specification is not meaningless as well as execute programs, if the specification makes sense.
AB - Many universities have courses and projects revolving around compiler or interpreter implementation as part of their degree programmes in computer science. In such teaching activities, tool support can be highly beneficial. While there are already several tools for assisting with development of the front end of compilers, tool support tapers off towards the back end, or requires more background experience than is expected of undergraduate students. Structural operational semantics is a useful and mathematically simple formalism for specifying the behaviour of programs and a specification lends itself well to implementation; in particular big-step or natural semantics is often a useful and simple approach. However, many students struggle with learning the notation and often come up with ill-defined and meaningless attempts at defining a structural operational semantics. A survey shows that students working on programming language projects feel that tool support is lacking and would be useful. Many of these problems encountered when developing a semantic definition are similar to problems encountered in programming, in particular ones that are essentially the result of type errors. We present a pedagogical metalanguage based on natural semantics, and its implementation, as an attempt to marry two notions: a syntax similar to textbook notation for natural semantics on the one hand, and automatic verification of some correctness properties on the other by means of a strong type discipline. The metalanguage and the tool provide the facilities for writing and executing specifications as a form of programming. The user can check that the specification is not meaningless as well as execute programs, if the specification makes sense.
UR - http://www.scopus.com/inward/record.url?scp=85139966610&partnerID=8YFLogxK
U2 - 10.4204/EPTCS.369.4
DO - 10.4204/EPTCS.369.4
M3 - Conference article
AN - SCOPUS:85139966610
VL - 369
SP - 51
EP - 66
JO - Electronic Proceedings in Theoretical Computer Science
JF - Electronic Proceedings in Theoretical Computer Science
SN - 2075-2180
T2 - 6th Working Formal Methods Symposium, FROM 2022
Y2 - 19 September 2022 through 20 September 2022
ER -
ID: 324681026