In the context of teaching computer science, many domainspecific 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.
原文链接
分享
引用
