描述和检查编程语言自然语义定义的工具
摘要：工具支持在大学编程课程和项目中对编译器和解释器的实现起着重要作用。前端编译器的开发已有多种工具支持，但在后端开发方面，工具支持相对较少，并且需要较高的背景经验，这对本科生来说并不适用。结构操作语义是一种用于指定程序行为的有用而数学简单的形式化方法，特别是大步语义或自然语义是一种常用且简单的方法。然而，许多学生在学习符号表示时困难重重，通常会出现定义结构操作语义的错误和无意义的尝试。调查显示，在编程语言项目中工作的学生认为缺乏工具支持，并且工具支持将是有用的。 在开发语义定义时遇到的许多问题与编程中遇到的问题相似，特别是那些实质上是类型错误的问题。 我们提出一种基于自然语义的教学元语言及其实现，试图将两个概念融合在一起：一方面是类似于教科书符号的自然语义，另一方面是通过强类型原则自动验证某些正确性属性。该元语言和工具提供编写和执行规范作为一种编程形式的功能。用户可以检查规范是否没有意义，以及如果规范有意义，则可以执行程序。
作者：Georgian-Vlad Saioc (Department of Computer Science Aarhus University, Denmark), Hans H"uttel (Department of Computer Science Aalborg University, Denmark, Department of Computer Science University of Copenhagen, Denmark)
论文ID：2209.09471
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-09-21