ELAN环境中基于重写逻辑的规范语言及其特性 - 理论计算机科学电子笔记65 No.3 (2002)

50理论计算机科学电子笔记65 No.3（2002）网址：http://www.elsevier.nl/locate/entcs/volume65.html7页ELAN环境：重写逻辑环境基于ASF+SDF技术- 系统演示-范登布兰德1Centrum voor Wiskunde en Informatica（CWI），Kruislaan 413，NL-1098 SJ阿姆斯特丹，荷兰LORIA-INRIA，615rueduJar dinBotanique，BP101，F-54602Viller s-le`s-NancyCedex，FranceP. - E.莫罗2LORIA-INRIA，615rueduJar dinBotanique，BP101，F-54602Viller s-le`s-NancyCedex，FranceC. Ringeissen3LORIA-INRIA，615rueduJar dinBotanique，BP101，F-54602Viller s-le`s-NancyCedex，France1介绍ELAN[10，3]是一种基于重写逻辑的规范语言[9，12]。 ELAN的一些特征是重写、AC匹配和控制由非融合重写系统引起的非确定性的策略。因此，AC匹配和策略是非确定性的两个来源。ELAN的特殊性包括在同一环境中集成两种形式的非确定性加上确定性的基于规则的计算。ELAN规范的开发是由一个环境支持的，其中包括一个解析器、一个解释器[10]和一个编译器[14，11]。这种环境可以被描述为基于命令行的。ELAN规范是使用标准编辑器开发的，并通过命令行提供给环境进行编译或解释。当前版本的ELAN编译器[11]是独立的1 电子邮件：Mark.van.den. cwi.nl，vandenbr@loria.fr2 电子邮件地址：moreau@loria.fr3 电子邮件地址：ringeiss@loria.frc 2002年由Elsevier Science B出版。诉 在CC BY-NC-ND许可下开放访问。51其余环境和数据交换基于REF（简化ELAN格式）[2]。ELAN可以用于各种问题的形式化规范，特别是在自动推理和约束求解领域。ELAN提供：一种基于（条件）项重写的通用代数规格说明形式。规格的模块化结构。关联交换重写。指导规则应用的策略。新ELAN环境的设计目标包括：开放性、适应性、可扩展性和组件的可重用性。旧的ELAN环境旧的ELAN环境可以被认为是一个单一的软件，很难维护，也不是真正开放的。例如，ELAN语法在解析器的当前实现中是“硬连接”的。语言的修改和扩展受到这种“硬连线”的阻碍此外，ELAN提供了预处理器语言结构，以自动生成给定规范文件的ELAN代码片段这种预处理机制可以看作是一种宏工具，它使用ELAN解释器来评估预处理器表达式，从而导致解析器和解释器之间的微妙交互。几年前，决定使用更通用的语言技术来设计和实现新的ELAN环境。这个想法是使用ASF+SDF解析技术来构建一个新的ELAN解析器，给定ELAN语法而没有预处理器语言结构，这不被视为ELAN语法的一部分[6]。ASF+SDF技术ASF+SDF元环境[4]中应用的技术也被认为是一种可能的解决方案，可以 改 善 ELAN 环 境 的 结 构 和 可 维 护 性 ， 并 使 语 言 扩 展 的 语 法 适 应ASF+SDF[8]是一种代数规范形式主义，用于定义（编程）语言的语法和语义。ASF+SDF元环境是一个集成的编程环境，用于开发这些语言定义并生成给定语言定义的编程环境。ASF+SDF的三项技术发展被证明对ELAN环境的开发非常有用，即ATerms [5]，ToolBus [1]和泛型解析技术[7]。ATerms格式是用于表示结构化信息（如（抽象）语法树、解析表、环境等）的通用工具总线是一种软件协调体系结构，52模块BasicStrategies[Sort]exports上下文无关语法id-> Sort {builtin（“id”）} fail-> Sort{builtin（“fail”）} first（{Sort“，"}+）-> Sort{builtin（“first”）}dc（{Sort“，"}+）-> Sort {builtin（“dc”）}...“repeat*"（排序）->排序{内置（“repeat”）}...Fig. 1.原始策略算子负责协调软件组件。通用语法分析技术由语法分析表生成器和语法分析器组成。解析器是一个无扫描的广义LR解析器（SGLR）[7]。2ELAN4.0这个新的ELAN环境的设计也导致了ELAN形式本身的完全重新设计。这个新的ELAN版本的语法已经完全改变。语法修改可以总结如下：签名定义被SDF替换。ELAN预处理器已被移除，并引入了固定的抽象语法和预定义的ELAN库来操作抽象语法树。通过这个库，可以开发在抽象语法树级别上创建和操作ELAN模块的ELAN每个排序的规则族被替换为单个规则列表。变量是按模块局部定义的，或按规范全局定义的，而不再是按规则族局部定义的。内置策略原语不再有固定的语法。策略操作符的定义方式与符号中的普通操作符相同。此外，战略规则和普通规则的定义之间的区别也消失了。新旧ELAN之间的一个重要区别是战略定义的方式。我们没有使用具有固定语法的内置策略原语，而是选择了一种更灵活的方法，其中策略是内置原语，但策略原语的确切语法在模块中定义。定义策略的模块的一部分如图1所示，图2显示了该策略模块的使用。53用户界面仪器总线模块Nqueens导入BuiltinInt基本策略[（BuiltinInt->BuiltinInt）]...图二.策略操作符图三. ELAN4.0环境3ELAN4.0环境ELAN 4.0环境的体系结构如图3所示。它由一个工具总线组成，该工具总线将以下组件互连：用户界面：系统的顶层用户界面。它主要由当前规范的导入图形的图形浏览器组成。文本编辑器：一个用于文本编辑的XEmacs。结构编辑器：与文本编辑器协同工作的语法导向编辑器。解析器：使用解析表参数化的SGLR解析器。解析表生成器：接受SDF定义作为输入，并为SGLR生成解析表。树存储库：存储模块、解析表等对应的所有术语。编译器：为规范生成C代码。解释器：通过解释执行规范。Unparser：pretty打印术语。4经验教训基于ASF+SDF技术的ELAN环境的设计和实现揭示了ASF+SDF元环境可以变得更加通用的一些点。解释器文本编辑器树存储库结构编辑器解析器可解析生成器Elan编译器解语法分析器54模块BuiltinInt...BuiltinInt“==”BuiltinInt-> BuiltinBool {builtin（“eq”）}...上下文无关语法“eq_int”（BuiltinInt，BuiltinInt）-> BuiltinBool{alias（BuiltinInt“==”BuiltinInt-> BuiltinBool {builtin（“eq”）}）}...见图4。使用别名4.1SDF扩展首先，为了表达所有ELAN特有的语法特征，SDF必须进行扩展。处理ELAN特定功能的SDF的三个主要扩展是：参数化排序，例如List[[BuiltinInt]]或List[[X]]，其中X是使用参数化排序List[[X]]的模块的参数实例化参数X也会导致List[[X]]的实例化策略排序，例如（BuiltinInt->BuiltinInt），它们与策略运算符结合使用。属性，它们用于定义生产规则的替代方案。SDF提供了“ELAN别名”的思想在规则和术语中，这两种选择都可以使用，但在内部只使用别名产生式规则。图4显示了使用alias属性定义Buil-tinInt的前缀相等运算符，作为中缀相等运算符的替代。4.2幅面差异化ASF+SDF元环境和ELAN环境都使用Aterms来表示解析表和语法树。然而，在ASF+SDF元环境中，组件之间只交换解析树，而ELAN环境既使用解析树又使用抽象语法树。ASF+SDF元环境的组件（如解释器、编译器和结构编辑器）使用解析树。然而，ELAN解释器和编译器使用抽象语法树，这使得有必要定义过滤器来将解析树映射到抽象语法树，反之亦然。从解析树到抽象语法树的映射实际上很简单，并且可以很好地本地化，但是从抽象语法树的映射是必不可少的，以便通过（结构）编辑器可视化范式。554.3结论ASF+SDF元环境非常通用。然而，在开发ELAN环境时，发现在某些地方，例如用户界面和树存储库，ASF特定信息是硬编码的。这些缺点很容易纠正。用扩展的SDF定义替换当前的SDF定义，或者从解析树切换到抽象语法树，需要对组件接口和组件本身进行更基本的修改。我们将继续在开发SDFMeta- Environment的方向上进行实验，该环境可以很容易地用ELAN、ASF、ESPGO等形式化来参数化确认我们要感谢Paul Klint和Jurgen Vinju关于改进元环境的通用性的建议。引用[1] J.A. Bergstra和P. Klint。离散时间工具总线Science of Computer Programming，31（2-3）：205[2] P. 我来回答你，S。Jamoussi，P. E. Moreau和Ch. 林盖森 处理ELAN通过交换格式重写程序 在proc [9] 1998年。[3] P. Bor ov ansk y' ， C. Kirchne r， H. Kirchne r， P.- E. Moreau和 Ch. 林盖 森ELAN概述。在[9]，1998的Proc.中。[4] M.G.J. van den Brand，A.作者声明：J. de Jong，M.德容，T. Kuipers，P. Klint，P. A.放大图片作者：J. Visser和J. Visser。ASF+SDF元环境 ： 一 个 基 于 语 法 的 语 言 开 发 环 境 。 In R. Wilhelm ， editor ， ChampierConstruction（CCSpringer-Verlag，2001.[5] M.G.J. van den Brand，H.A. de Jong，P. Klint，and P.A.奥利维尔有效的注释条款。软件，实践经验，30（3）：259[6] M.G.J. van den Brand和C.林盖森ASF+SDF解析工具应用于ELAN。在KokichiFutatsugi ， 编 辑 ， 理 论 计 算 机 科 学 电 子 笔 记 ， 第 36 卷 。 Elsevier SciencePublishers，2001.[7] M.G.J. van den Brand、J. Scheerder、J.J. Vinju和E.维瑟无扫描广义LR解析器的消歧过滤器。在N. Horspool，编辑，《建筑》（CC《计算机科学讲义》，页？？- ？？Springer-Verlag，2002.[8] A. van Deursen，J. Heering，and P. Klint，editors. 语言原型，第5卷，AMAST系列计算机。世界科学，1996年。56[9] C. Kirchner和H.基什内尔，编辑。第二国际机场重写逻辑及其应用研讨会，理论计算机科学电子笔记，Pont-a`-Mousson（法国），1998年。爱思唯尔[10] C. Kirchner，H. Kirchner，and M.维特克使用计算系统设计约束逻辑程序设计语言。在P. Van Hentenryck和V. Saraswat，编辑，约束编程的原理和实践。纽波特文件。第131-158页。麻省理工学院出版社，1995年。[11] 他是基什内尔和皮埃尔-艾蒂安·莫罗。将重写提升为编程语言：在关联-交换理论中的非确定重写程序。Journal of Functional Programming，11（2）：207[12] 何塞·梅瑟格尔。 作为并发统一模型的条件重写逻辑。Theoretical Computer Science，96（1）：73[13] E. 维 瑟 Replego ： 一 种 基 于 重 写 策 略 的 程 序 转 换 语 言 。 系 统 描 述 ： 以 .Middeldorp，编辑，RTASpringer-Verlag，2001.[14] M.维特克 一种非确定性项重写系统的编译器。 Harald Ganzinger，编辑，Proceedings 7th Conference on Rewriting Techniques and Applications，新不伦瑞克（新泽西州，美国），计算机科学讲义第1103卷，第154-168页。Springer-Verlag，1996.