DynSem: A DSL for Dynamic Semantics Specification
DynSem: A DSL for Dynamic Semantics Specification
复制标题
DynSem：动态语义规范的 DSL
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
E. Visser
中科院分区：
文献类型：
--
作者：
V. Vergu;P. Néron;E. Visser
编程语言的形式定义、语义及其实现通常是单独定义的，存在发散的风险，使得形式语义的属性不是实现的属性。在本文中，我们提出了 DynSem，一种用于规范编程语言动态语义的领域特定语言，旨在支持形式推理和高效解释。 DynSem 通过静态类型的条件术语缩减规则支持语言操作语义的规范。 DynSem 通过提供基于归约箭头和隐式项构造函数的隐式构建和匹配强制来支持归约规则的简洁规范。 DynSem 通过采用来自 I-MSOS 的语义组件的隐式传播来支持模块化规范，这允许从不影响这些组件的规则中省略环境和存储等组件的传播。 DynSem 支持声明本机运算符，以将语义的各个方面委托给外部定义或实现。 DynSem 支持辅助元函数的定义，可以使用常规约简规则来表达辅助元函数，并服从语义组件传播。 DynSem 规范可通过自动生成基于 Java 的 AST 解释器来执行。
The formal definition the semantics of a programming language and its implementation are typically separately defined, with the risk of divergence such that properties of the formal semantics are not properties of the implementation. In this paper, we present DynSem, a domain-specific language for the specification of the dynamic semantics of programming languages that aims at supporting both formal reasoning and efficient interpretation. DynSem supports the specification of the operational semantics of a language by means of statically typed conditional term reduction rules. DynSem supports concise specification of reduction rules by providing implicit build and match coercions based on reduction arrows and implicit term constructors. DynSem supports modular specification by adopting implicit propagation of semantic components from I-MSOS, which allows omitting propagation of components such as environments and stores from rules that do not affect those. DynSem supports the declaration of native operators for delegation of aspects of the semantics to an external definition or implementation. DynSem supports the definition of auxiliary meta-functions, which can be expressed using regular reduction rules and are subject to semantic component propagation. DynSem specifications are executable through automatic generation of a Java-based AST interpreter.