基于XML的SOSDT集成环境：结构操作语义规范开发工具（2007）

理论计算机科学电子笔记175（2007）71-75www.elsevier.com/locate/entcs一个基于XML的可执行结构操作语义规范开发集成环境Adrian Pop1，2Peter Fritzson3李国平大学计算机与信息科学系程序设计环境实验室Linkopingg，Sweden摘要结构操作语义开发工具（SOSDT）Eclipse插件将关系元语言（RML）编译器和调试器与Eclipse集成开发环境框架集成在一起。SOSDT与RML编译器和调试器一起，为开发提供了一个环境，检查和维护可执行的结构操作语义规范，包括SOS规范的自然语义大步变体。RML语言在我们部门成功地用于为Java、Modelica、Pascal、MiniML等一系列语言编写大型规范。SOSDT环境包括对浏览、通过菜单或弹出窗口完成代码、代码检查、自动缩进和规范调试的支持关键词：SOS，自然语义，可执行规范，Eclipse，RML，调试。1引言如果没有一套强大的工具（包括执行、调试和分析）的支持，任何编程语言环境都不能被认为是成熟的在本文中，我们提出了一个集成开发环境，称为结构操作语义开发工具（SOSDT）[4]，用于浏览，检查和调试语义规范。SOSDT环境基于现有的关系元语言（RML）系统及其调试器，并为这些系统提供了一个易于使用的图形界面1这项研究得到了国立计算机科学研究生院（CUGS）和SSF RISE项目的部分支持。2电子邮件地址：adrpo@ida.liu.se3电子邮件地址：petfr@ida.liu.se1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.11.01972A. Pops，P.Fritzson/Electronic Notes in Theoretical Computer Science 175（2007）712SOS/Natural语义学与关系Meta- Language（RML）自然语义学[2]是一种形式主义，用于指定编程语言的许多方面，例如类型系统，动态语义，翻译语义，静态语义等。自然语义学是一种操作语义学，它来源于Plotkin[6]结构操作语义学，结合了自然演绎的微积分关系元语言（Relational Meta-Language，RML）是一种用于编写可执行SOS/自然语义规范的实用语言。RML语言被广泛用于教学和编写不同语言的大型规范，如Java，Modelica，MiniML，Pascal等。RML语言由rml2c编译器编译为高效的C代码通过这种方式，编译器的大部分从RML语言的特点可以看出：强静态类型，简单的模块系统，类型推理，模式匹配和递归用于控制流程，类型可以是多态的。正如在[3]中指出的，计算机科学界总是忽视调试问题，即使软件开发的调试阶段花费的时间比整个开发时间要多即使RML语言的学习曲线很短，但由于缺乏调试工具，以前在理解、调试和验证大型规范方面存在问题。我们已经通过为RML提供一个调试框架解决了调试问题[7]。调试器基于RML编译器中的抽象语法树插装（程序转换）和一些运行时支持。类型重构在运行时执行，以呈现用户定义的类型的值3作为Eclipse插件SOSDT（以前称为RML开发工具（RDT））环境为我们的工具提供了一个集成环境图1和图2显示了带有调试和组件之间各种交互的集成环境。SOSDT环境有三个主要组件：RML编辑器、RML浏览器和RML浏览器组件。当在Eclipse环境中选择SOSDT透视图时，所有组件都是活动的。Eclipse中的透视图用于配置与特定项目相关的视图。在SOSDT环境中，用户通过向导创建和管理RML项目和RML文件RML编辑器组件提供语法突出显示、自动缩进、代码完成、类型信息和错误突出显示。该组件从RML解析器和RML查询器获取所需的信息。从RML查询器收集错误和类型推断信息。的类型A. Pops，P.Fritzson/Electronic Notes in Theoretical Computer Science 175（2007）7173Fig. 1. RML系统和SOSDT环境的体系结构。图二. 用于RML开发的Eclipse插件。74A. Pops，P.Fritzson/Electronic Notes in Theoretical Computer Science 175（2007）71当悬停在变量、关系或模式上时显示信息。当用户编写关系调用或模式时提供代码完成RML浏览器组件提供了在文件中轻松导航的功能RML解析器用于收集浏览所需的信息。每个RML文件的类型、值、关系和规则都显示在一个树中。RML调试组件通过套接字与RML调试框架进行通信，以提供调试工具，如断点、运行和步进、变量值检查等。所有SOSDT组件都使用Eclipse框架的组件，这些组件都使用来自RML解析器和RML解析器的信息填充当文件被保存时，RML解析器读取文件并更新内部RML模型信息，从而触发RML浏览器的更新。此外，在保存时，RML文件被发送到RML编译器，该编译器转储要在问题视图中显示的错误信息和用于更新内部RML模型的类型信息。4绩效评价下表所用的测试用例基于MiniFreja语言[5]的可执行规范（SOS/RML中的自然语义），运行基于Eratosthenes筛选的测试程序。复制测试所需的所有信息可在http://www.ida.liu.se/adrpo/sosdt/tests获得。Mini-Freja是一种按名称调用的纯函数式语言。 测试程序计算-识 别 质 数 Prolog 翻 译 （ mf.pl ） 最 初 由 Mikael Pettersson 实 现 比 较 是 在FedoraCore4Linux机器上进行的，该机器配备两个1500 MHz和1.5GB的AMDAthlon（TM）XP 1800+处理器 记忆。测量于2006年4月进行。预充编号RMLSICStusSWIMaude-MSOS-工具80.000.050.002.92300.021.421.79226.77400.063.483.879-500.13-11.339-1001.25- -20016.32- -执行时间以秒为单位。该符号表示内存不足。RML的内存消耗达到峰值9Mb。其他系统消耗了整个1.5Gb的内存，并在大约40个素数时中止。到目前为止，使用RML开发的最大的可执行规范是Modelica语言规范（一种基于方程的语言），大约有80000行。我们已经提高了编译速度超过10倍，因为一年前编译80000行RML现在需要不到一分钟的1.5 GHz的笔记本电脑。A. Pops，P.Fritzson/Electronic Notes in Theoretical Computer Science 175（2007）71755结论和今后的工作我们使用RML为几种不同的编程语言编写SOS/自然语义风格的大型可执行规范的经验表明，支持开发环境对于开发规范也是必不可少的。因此，我们设计并实现了一个集成环境的原型来支持这种开发，首先是部分基于Emacs的版本，目前作为一个SOSDT Eclipse插件集成在Eclipse中。我们的部分RML用户使用此环境的原型调试其规格，并向我们提供正面反馈及各种改进建议虽然这是一个良好的开端，但可以对该环境进行许多改进。在未来，我们计划提高调试器的执行速度，并实现额外的功能。我们的目标是为基于Eclipse平台的RML提供一个集成良好的支持性开发环境（IDE）引用[1] Eclipse开发平台，http://www.eclipse.org。[2] Kahn，G.， 自然语义学，在：未来一代计算机的编程。ed Niva M.，p. 237.258，1998年。[3] 利伯曼，H.，调试丑闻和如何处理它，在：ACM的通信。第40（4）卷，第27-29页，1997年。[4] 结构操作语义开发工具（SOSDT）Eclipse插件，http://www.ida.liu.se/www.example.com[5] 拜托，M.，“C om piling n g N a tur a l S e m a n t i c s，”P h. D. 这是，LinkéopingUniversity（1995），DisseltationNo.四一三，也可参见Lecture Notes in Computer Science（LNCS）1549，Springer-Verlag，1999，RMLSite：http://www.ida.liu.se/labs/pelab/rml。[6] Plotkin，G. D、A Structural Approach to Operational Semantics，in：The Journal of Logic andAlgebraic Programming 60-61，17-139. ，2004年。[7] Pop，A.和p.Fritzson，《自然语义规范》，载于：第六届自动化和分析驱动语义国际，2005年，加利福尼亚州蒙特雷。