In the context of teaching computer science, many domain-specific languages (DSLs) used for data manipulation and transformation follow imperative paradigms, yet their semantics remain informal or tool-dependent. This paper proposes a pedagogical framework based on executable formal semantics to improve conceptual understanding and practical competence in such DSLs. Using a minimal imperative DSL developed as a teaching tool to illustrate arithmetic and data transformations, we define its syntax and semantics using denotational semantics and develop an executable interpreter directly derived from the formal rules. The framework enables students to explore and visualize the effects of each language construct, reason about program behavior, and verify correctness properties. We present a case study in which we focus on the gradual use of cross-curricular relationships and gradually build a comprehensive package for students that draws on knowledge from several courses focused on formal methods in software engineering. The paper concludes with a discussion of the potential of this methodology to bridge the gap between formal methods and practical education in the field of computer science.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Executable Semantics for Teaching Concatenative Stack-Based DSLs: The Case of StackLang

  • William Steingartner,
  • Wolfgang Schreiner

摘要

In the context of teaching computer science, many domain-specific languages (DSLs) used for data manipulation and transformation follow imperative paradigms, yet their semantics remain informal or tool-dependent. This paper proposes a pedagogical framework based on executable formal semantics to improve conceptual understanding and practical competence in such DSLs. Using a minimal imperative DSL developed as a teaching tool to illustrate arithmetic and data transformations, we define its syntax and semantics using denotational semantics and develop an executable interpreter directly derived from the formal rules. The framework enables students to explore and visualize the effects of each language construct, reason about program behavior, and verify correctness properties. We present a case study in which we focus on the gradual use of cross-curricular relationships and gradually build a comprehensive package for students that draws on knowledge from several courses focused on formal methods in software engineering. The paper concludes with a discussion of the potential of this methodology to bridge the gap between formal methods and practical education in the field of computer science.