重写逻辑语义定义框架K及其在编程语言解释器中的应用

理论计算机科学电子笔记176（2007）215-231www.elsevier.com/locate/entcs语言定义和高效解释器生成MarkHillsa，1TraianSerbanutaa，2GrigoreRosua，3美国伊利诺伊大学香槟分校计算机科学系201 N Goodwin Ave，Urbana，IL 61801摘要本文介绍了一种用于编程语言的重写逻辑语义定义框架，称为K，并将K语言定义部分自动地翻译成重写逻辑和C语言。该框架以定义SILF为例，SILF是一种带有函数的简单命令式语言。 翻译将K定义转换为重写逻辑使得能够使用为重写逻辑规范开发的各种分析工具，而转换为C则允许非常高效的解释器。一组测试显示了从K定义编译的解释器的性能。保留字：编程语言，重写逻辑，语言解释器。1引言K语言定义框架[9]是一个基于重写逻辑的框架，用于指定编程语言。它包括一个记法，K-记法，由一系列特定于领域的语法糖约定组成，旨在简化和增强语言定义的可读性，以及一种语言定义技术，K-技术，基于一阶表示的延续。 作为我们正在进行的研究的一部分，我们正在围绕K开发一些工具，以帮助定义和分析编程语言。在这里，我们展示两件作品。首先，我们展示了一个简单的编程语言的语义，函数是用K定义的。这种语言具有标准的命令式特性，包括以函数返回形式的受控跳转。其次，我们提供了从我们的K符号到一个由NSF资助CCR 0234524、CCF-0448501和CNS-0509321支持1电子邮件：mhills@cs.uiuc.edu2电子邮件：tserban2@cs.uiuc.edu3电子邮件：grosu@cs.uiuc.edu1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.06.017216M. Hills等人/理论计算机科学电子笔记176（2007）215··语言的解释器，用C编写。 我们正在积极致力于提供K语言定义的口译员的自动化构建，目前有一个半自动化的翻译。在第2节中，我们将概述K表示法以及如何将其转换为重写逻辑的细节。在第3节中， 我们通过 定义带函 数的简单 命令语 言（Simple Imperative Language withFunctions，简称SILF）来展示K的工作。在第4节中，我们提供了从K到C的翻译细节，包括与其他语言编写的等效程序进行比较的一些初始性能数据。第4节讨论了相关的工作，而第5节讨论了未来的工作，并结束了论文。第二章K语言定义框架在这里，我们简要回顾一下K-框架[9]，它对重写逻辑中的紧凑，模块化和直观地定义语言很有用。它由K符号组成，即， 一系列用于匹配模公理、用于省略不必要的变量、用于排序推理、用于上下文转换器的记法约定，以及K-技术，这是一种基于延拓的代数定义语言的技术。K-框架在[9]中有详细描述匹配模尽管它的一般棘手[3]，匹配模Asociativity ，Ccommutativity ，和Iidentity，或ACI匹配，往往是相对有效的在实践中。许多重写引擎支持它的全部通用性。ACI匹配导致紧凑和优雅，但有效地可执行的规范。不同的语言有不同的方式来说明二元运算是关联的和/或交换的和/或具有恒等式;为了保持讨论的通用性，我们假设所有的ACI运算都使用mix fix连接符号“”来编写，并且具有恒等式““，而除了一个之外，所有的4个AI运算都使用逗号符号“，“并且也具有恒等式”“。特别是在K规范的实现中，为了避免混淆，人们可能希望为不同的ACI或AI操作使用不同的名称。ACI操作对应于多集合，而AI操作对应于列表。因此，对于任何排序Sort，我们巧妙地添加Sort的超级组ACI操作将用于将状态定义为属性的“汤”;例如，语言的状态可以是包含存储、忙的锁、输入/输出缓冲器等的“汤”，以及一组线程。汤可以是嵌套的;例如，一个线程本身可以包含一个线程属性汤，如一个环境、它持有的一组锁、几个堆栈（用于函数、异常、循环等）;环境更进一步是一个由对（名称、位置）等组成的汤。列表将用于指定属性顺序很重要的结构，例如缓冲区[4] AI运算的逗号符号的例外是M. Hills等人/理论计算机科学电子笔记176（2007）215217→∀×××→×→× ×→(for输入/输出）、函数的参数等。比如说， 让我们定义一个操作更新：Environment Name LocationEnvironment，其中Environment是与具有一个构造函数配对操作的配对排序NameLocation相关联的集合排序NameLocationSet（，） ：名称位置名称位置。update（Env，X，L）与Env相同，只是X的位置不同，应该用L替换：（X：名称; L，LJ：位置; Env：环境）更新（（X，LJ）Env，X，L）=（X，L）Env。ACI匹配算法排序推理。令人惊讶的是，update等式中的变量声明部分几乎占了句子长度的一半。在我们用Maude定义语言的实验中，经常会出现这样的情况：变量声明占用大量的空间，有时甚至超过整个语言规范的一半。然而，在大多数情况下，变量的种类可以从上下文自动推断。为了简化这个过程，我们假设所有变量名都以大写字母开头。考虑，例如，上述等式的两项，更新（（X，L，J）Env，X，L）和（X，L）Env。由于更新的优先级是环境名称位置环境，我们可以立即推断出X和L的排序分别是Name和Location。此外，由于更新的第一个参数具有排序环境，并且由于环境是使用操作构造的，：环境环境环境，可以推断这种Env就是Environment。由于子排序，出现在术语中某个位置的变量可能有多个排序。例如，上面的变量Env可以同时具有排序Environment（别名NameLocationSet）和排序NameLocation。该报告[9]更深入地讨论了在存在子排序的情况下排序推理的微妙之处。这里我们只记得，如果一个变量的出现可以有多个排序，我们默认地或按照惯例假设，这个变量出现在它可以有的那些排序中具有最大的排序;这个惯例对应于我们假设关于每个变量出现的“最少”信息的直觉。如果同一个变量出现在多个位置上，那么我们就为该变量推断出它在其中所能具有的“最具体”排序。 从技术上讲，这是为该变量在其出现的不同位置上推断的所有最大排序的交集。 如果变量的排序推理过程是模糊的，或者如果一个人不确定，或者如果一个人真的想要一个不同于推断的排序，或者甚至只是为了清楚起见，一个人可以对变量进行排序：我们使用“：”将排序附加到变量，例如，X：排序。例如，从术语update（Env，X，L），我们只能推断出Env的类型是Environment，在这种情况下最一般的可能。 如果出于任何原因，一个人想提到一个“特殊”的环境，如果只有一对，则可以写入update（Env：NameLocation，X，L）。下划线变量和元组。 使用排序推理约定，218M. Hills等人/理论计算机科学电子笔记176（2007）215→因此，定义操作更新的等式可以写为update（（X，LJ）Env，X，L）=（X，L）Env.注意，不需要出现在lhs中的位置LJ它只是说名称X被分配在某个位置，但我们不关心那个位置是什么（我们无论如何都要改变它）。由于这在我们的语言定义中是一种常见的现象，我们可以自由地用下划线代替不必要的字母变量，就像在Prolog中一样。 因此，我们建议， 上面的等式可以写成update（（X，）Env，X，L）=（X，L）Env.就像我们需要将名称和位置配对来创建环境一样，我们经常需要将两个或多个术语元组化，以便“保存”当前信息以供以后处理。在K中，按照惯例，我们允许所有的元组操作，而不明确定义它们像变量的种类一样，它们的属性也可以从上下文中推断具体地，如果项（X1：Sort1，X2：Sort2，. . .，Xn：Sortn）出现在某些上下文中（变量sort可以被推断），那么我们隐式地将sortSort1Sort 2. Sortn和操作（，，...，）：Sort1 × Sort2 ×···× Sortn → Sort1Sort2.算是吧重写规则的上下文表示法。所有后续的重写规则将只应用于一个（大）项，对程序的状态进行编码。具体来说，它们中的大多数将适用于通过匹配选择的子项，但只有在国家结构允许的情况下。换 句话说，我们的大多数规则都是C[t1] ··· [tn] → C [TJ1] ··· [TJn]的形式，其中C是具有n ≥ 0“洞”的上下文项，并且t1，.，tn是需要替换为tJ1，.，在这种情况下， C不需要匹配整个状态，但有时它可能非常大。为了简化符号和便于阅读，在K中我们将规则写为C[t1] ··· [tn]。tJ1t Jn这种表示法遵循一种自然的直觉：首先写出要进行转换的状态上下文，然后在需要更改的内容下面加下划线，然后将更改写在这条线下面。我们上面的上下文符号被证明在与““变量组合时特别有用匹配前缀、后缀和片段。我们在这里介绍另一种符号，它将帮助我们进一步压缩语言定义，消除不必要的下划线变量。许多状态属性“soup”将使用特定的操作符进行包装，以使它们与其他soup区分开来。 例如，在将环境放置到线程的状态属性汤中之前，环境将使用操作env：EnvironmentAttribute因此，如果我们想找到一个名字X在环境中的位置M. Hills等人/理论计算机科学电子笔记176（2007）215219◦◦⟩◦◦⟨⟩·⟨ ⟩⟨ ⟩⟨···⟨··然后我们将环境属性与“模式”项env（（X，L））进行匹配，从而找到所需的位置L ;下划线变量匹配环境的其余部分。 下划线使模式术语看起来比需要的更重，更难阅读，特别是当状态使用深度嵌套的属性汤定义时（本文中不是这种情况）。上面我们真正想说的是，我们对出现在环境中某处的对（X，L）感兴趣在我们特定的语言定义领域，我们主观地认为，对于同一个模式项，用env（X，L）表示比用下划线表示更好。按照惯例，只要att（T）（即，左括号直角）作为语法糖用于att（T），attT）（即，左角右括号）作为att（T）的句法糖，att T（即，左角和右角）作为att（T）的句法糖如果这种符号的直观性来自于这样一个事实，即左和右的角度可以被看作是相应的“方向”和括号之间的某种混合。例如，如果 类似地，T）说T是一个suprix，T说T是一个被att包装的列表中的连续片段。如果““也是可交换的，即，一个ACI运算符，那么前缀、后缀和片段的概念是等价的，都说T是被att包裹的集合的子集。这种记法惯例在与K记法的其他惯例部分结合使用时特别有用例如，在续集中定义的编程语言的输入和输出将被建模为逗号分隔的整数列表，使用AI二进制操作 ，in（N1，N2，and，respectively，out·）·N1、N2第一个匹配缓冲器中的前两个整数并删除它们（行下面的““），而第二个匹配缓冲器的结尾（行上面的““）并将两个整数追加到注意，后者之所以有效，是因为匹配模标识：out）是out（，）的简写，其中下划线匹配整个列表;用列表N 1，N 2替换““只不过是将两个作为另一个有趣的示例，这次使用ACI运算符，请考虑更改位置220M. Hills等人/理论计算机科学电子笔记176（2007）215将环境中的标识符I映射到另一个位置，比如L;当具有相同标识符I的变量被局部声明并因此被“阴影”时，这在允许局部变量声明的语言的定义中可能是必要的。以前声明的同名变量。 这可以通过以下方式实现（更大背景的env（I，）。L上下文变换器是K表示法中最微妙的方面，基于这样的观察：在编程语言的定义中，程序的状态在程序执行期间总是不会改变其重要结构。例如，存储将始终保持在状态结构中的同一级别，通常在顶层。如果已知某些状态基础结构在任何程序的评估期间保持不变，并且如果人们对可以明确地位于该状态基础结构中的某些属性感兴趣，则我们仅提及那些属性作为上下文的一部分，假设其余的可以自动地（静态地）生成部分上下文。 由于SILF没有线程、异常或其他复杂的控制敏感语言特性，上下文转换器在本文中没有区别，因此我们不详细讨论它们。对上下文转换器在语言定义的紧凑性和模块性中的作用感兴趣的读者可以参考[9]。把K翻译成Maude。我们目前手动执行从K规则到Maude[1]的翻译，并正在进行自动翻译。作为一个例子，考虑下面所示的规则，它是用于函数应用的：k（val（）aapply（I）aK）fstack（·env（Env）fenv（I，KJ）genv（GEnv）KJ（环境，K）GEnv换句话说，这条规则规定，要将标识符为I的函数应用于一个（可能是空的）值列表，我们需要将applycontinuation item和continuationK替换为函数环境中与函数I相关联的continuationKJ，将K和环境Env放在堆栈上，并将Env替换为全局环境GEnv，这将使我们能够访问全局名称，同时隐藏在调用上下文中声明的名称。我们在这条规则中使用了我们在本节中讨论的许多约定。例如，这些值是未命名的，因为我们现在不使用它们。此外，由于堆栈是一个关联列表，我们通过将左侧的标识替换为我们正在堆叠的项（元组）来向列表的头部添加内容。函数环境是一个集合，因此我们匹配函数名以获得集合中的正确元组，而无需指定集合的其余部分。我们只需要通过把变化放在变化的东西下面来标记那些正在变化的状态部分;保持不变的状态部分不需要进一步的符号。为了进行比较，这里是这个规则的Maude方程，包括变量声明。对于出现在这两个中的变量，使用了与上面相同的变量名：varI：Id. vars K K ' ： C o n t i n u a t i o n .M. Hills等人/理论计算机科学电子笔记176（2007）215221× ×−→Int egerbubblersN：：=（+|-）？（0个.. 9）+声明D：：=var I|变量I [N]表达式E：：=N |E + E |E-E |E * E |E/E |E %E|-E|E E |E>= E |E = E |E！= E|E和E |E或E|不是E |N |I（El）|I [E]|我|读表达式列表El：：=E（，E）|无声明S：：=I：= E |I [E]：= E|如果E，则S|如果E那么S否则S|对于I：= E to E do S od |while E do S od |S; S|D|I（El）|回路E |write E函数声明FD：：=function I（Il）begin S end标识符I：：=（a − zA − Z）（a − zA − Z0− 9）标识符列表Il：：=I（，I）|虚空P rog ramsPgm：：=S？FD+Fig. 1. 关于SILFvarICS：< Continuation>Set. var Vl：ValueList. varECL：<< Location>Set>List.vars Env GEnv：< Location>Set。等式k（val（VI）-> apply（I）-> K）fstack（ECL）env（Env）fenv（ICS [I，k（val（VI）-> K ' ） f s t a c k （ [ E n v ， K ] ， E C L ） e n v（ G E n v ） f e n v （ I C S [ I ， K ' ] ） g e n v （ G E n v ） .注意这里我们首先需要声明一些变量。此外，请注意，我们需要命名我们不关心的项目，例如值列表，并且我们还需要将左侧提到的项目包含在右侧，即使它们没有变化。3 SILF：一种简单的命令式语言使用K符号，我们现在定义一个简单的命令式语言，我们在这里将其称为SILF。SILF的BNF语法如图所示1.一、请注意，程序由一个可选语句组成，该语句被假设为全局变量声明（而不仅仅是任意语句），后跟一个或多个函数，其中一个应该称为main。下面我们假设程序格式良好，类型正确，并且我们不需要担心诸如优先级之类的问题。我们在代数记法中采用了mix-fix表示法来表示语法，并进行了标准转换，为每个非终结符添加了一个新的排序，为每个产生式添加了一个新的操作。例如，函数的声明将是：function（）beginend：IDIdListStmtFunDecl. 在下面的规则中，垂直线偶尔用于分隔同一行上的规则（例如，在下面的函数返回规则中）。这些垂直线没有语义意义。国家基础设施。由于下面给出的语义中的规则作用于SILF状态，因此理解状态结构很重要。程序的状态是由状态“汤”中的一些“配料”组成的，在本例中都是顶级的由k指示的延续保持跟踪当前控件上下文。fstack是函数栈，保存有关222M. Hills等人/理论计算机科学电子笔记176（2007）215返回时恢复计算-这类似于堆栈帧。 环境和genv保存本地和全局环境的名称到位置的映射，而fenv保存从函数名称到主体的延续的映射。存储保存位置到值的映射。输入和输出分别用in和out表示。最后，使用nextLoc跟踪存储中要分配的下一个位置。这在图2中以图形方式表示。形式上，通过代数签名声明状态结构，其中每个“成分”由我们称为“at- tribute”的适当操作包装，并且其中成分通过AC级联操作在“汤”中。一些汤的成分是列表（例如，I/O“缓冲器”、函数栈、延续），其他是集合（例如，环境，商店），而其他只是普通的数字（例如，下一个位置）。就像图1中与BNF相关的混合代数签名一样，我们在这里也不定义状态签名，因为它很简单。当一个程序被执行时，我们需要构造它的初始状态。我们使用一个eval操作来实现这一点。 对于SILF，此操作将采用程序Pgm，整数N1的输入列表，并将评估（Pgm，Nl）k（Pgm）fstack（·）env（·）genv（·）fenv（·）input（ Nl）output（·）store（·）nextLoc（0）由k包装的延续结构保持要执行的任务的有序列表以继续计算。我们添加了额外的排序来表示抽象语法，包括值（V）、环境（Env）、延续（K）、位置（L）和存储（Mem），并为每个排序添加了适当的列表和集合程序. 一个程序由许多全局变量声明组成，后面跟着许多函数。 这些功能没有固有的顺序-所有功能都可以看到所有其他功能。 要执行一个程序，我们需要处理所有的全局变量声明，创建全局环境，处理所有的函数声明，然后调用main函数：k（pgm（SFD））stmt（S）amkGenvafdecl（FD）astmt（main（））如何处理stmt（S）将在本节后面描述可以查看stmt（S）图二. SILF国家基础设施k fstackenv（X1，L1）genv（X1，L1）存储（L1，V1）在下一个位置3，8，2，5，6，9，0fenv（F1，K1）（Ln，Vn）…出来3,6,7,8,9,1M. Hills等人/理论计算机科学电子笔记176（2007）215223和exp（E）作为 如前所述，当S只包含变量声明时，stmt（S） 在延续的顶部，最终在属性env中产生相应的环境。然后，mkGenv只需要将该环境移动到genv中（这将允许我们稍后轻松引用全局变量environment）：2019 - 05 - 22 00：00：0000：00·函数声明被逐个处理）Envfdecl（FD：FunDeclFD：FunDeclNeSet）fdecl（FD）afdecl（FD）功能协调发展的函数语义包括三个主要的构造：函数声明、函数调用和函数返回。下面我们依次介绍。 我们首先需要将声明的函数添加到函数环境中。 我们假设函数名是不同的，并且声明都发生在函数的开头。我们在函数体中添加了必要的结构来将输入值绑定到形参，所以我们不需要在调用语义中添加它（bind的语义将很快给出k（fdecl（functionI（Is）beginSend））fenv··（I，bind（Is）astmt（S））函数可以用作表达式或语句：exp（I（El））stmt（I（El））exp（El）aapply（I）exp（El）a应用（I）a丢弃当在延续的顶部时，延续项exp（El）评估表达式E1的列表，并产生它们相应的值，即val（V1）形式的项。当用作语句时，我们将丢弃延续项放入延续中，以丢弃返回值（这将很快定义）。一旦参数被求值，我们就可以应用函数了。由于函数被存储为标识符/延续对，因此我们可以直接取出延续 为功能。此外，我们保存了当前的continuation和环境，以便在返回时退出函数时可以快速恢复它们k（val（）aapply（I）aK）fstack（·env（Env）fenv（I，KJ）genv（GEnv）KJ（环境，K）GEnv当我们遇到一个返回时，首先我们需要计算我们要返回的值的表达式一旦计算出值，我们就可以将上下文切换回调用者，我们通过将当前环境和continuation替换为保存在函数堆栈顶部的环境和continuation来stmt（returnE）exp（E）返回）k（val（）a返回aK）fstack（（Env，K）env（·）Env州助理运营。SILF语义中的许多规则对状态执行类似的更改。 我们已经将这些变化抽象为一些规则，然后可以跨语义的不同部分使用。操作bind在环境中创建新绑定此操作绑定一个值列表224M. Hills等人/理论计算机科学电子笔记176（2007）215←添加到标识符列表，将标识符添加到环境中，将值添加到存储中，并通过共享位置链接。为了在没有值的环境中创建新绑定，我们使用绑定操作的变体，它将标识符列表绑定到位置列表，但不改变存储（len是列表上的常见长度操作，Ll是位置列表（L，L+1，...，L+len（Il）− 1））：k（val（Vl）abind（Il）env（Env）商店（Mem）nextLoc（L ）·Env[Il←Ll]记忆[Ll←Vl]L+len（Il）k（bind（Il）env（Env）nextLoc（L）·Env[Il←locs（L，len（Il））]L+len（Il）[]操作将正确地更新集合，使用左侧的列表作为一个“键”列表，可以将新的键/值对添加到集合中，或者用新的键/值对替换现有的键/值对。定义很简单，这里没有显示。我们还可以绑定存储块。这只会将第一个位置绑定到标识符，然后将下一个位置提前任意数量。 这可以用来表示为数组分配内存块k（val（int（N））abindBlock（I）env（Env）nextLoc（L）·Env[I ←L]L+N对于赋值，assignTo分两步为store赋值，首先将标识符赋值（assignTo）转换为位置赋值（assignToLoc），然后执行赋值：k（val（ V）aassignTo（I）赋值给（I，L）assignToLoc（L）k（val（V）aassignToLoc（L）存储（Mem ）·记忆[L←V]我们也有一个类似的数组版本，它将在一个o数组集上赋值int n（i，j）{n（I，j）{n（ I，j）}val（V）aassignToLoc（L+N）类似地，我们有两个查找操作：k（lookupLoc（L））store（L，V）k（val（int（N））alookupO set（I）env（I，L）val（V）lookupLoc（L+N）有时我们会想从continuation中丢弃一个值为此，我们使用具有以下语义的discard：k（val（V）adiscard·变量声明。在SILF中，我们有两种不同类型的变量声明-整数和整数数组。数组只能声明为固定大小（正整数）。在这两种情况下，声明都没有设置初始值-这对应于在赋值之前内存中的“垃圾”概念，并且任何读取“垃圾”的尝试都将失败。我们对待数组的方式与C相同（数组的索引为0，因此10个元素的数组的索引为0到9），数组的位置 名称与位置0相同M. Hills等人/理论计算机科学电子笔记176（2007）215225stmt（变量I）stmt（varI[N]）bind（I）val（int（N））abindBlock（I）查找和简单表达式。SILF的一些最基本的表达式是名称和索引数组值的查找，以及文字表达式。对于一个字面整数，我们只返回一个封装在值包装器中的整数值exp（N） . 对于标识符和数组，我们返回当前值，或者int n（intN）分配给标识符或数组的给定元素。 我们会处理的 分两步，首先检索值k（exp（I））≠env（I，L）≠lookupLoc（L）算术、关系和逻辑运算。所有三种操作类型都遵循相同的一般模式。当我们遇到加法表达式时，例如，我们首先需要对两个操作数求值。我们还需要跟踪我们正在执行的操作。因此，我们将替换一个表达式，如E+EJ，如果我们评估E和EJ，并将+放在延续上，以提醒我们需要对结果做什么。一旦我们在a +的顶部计算两个表达式（这里，预期都是整数），我们返回它们的总和（使用整数加法）：exp（E+EJ）val（int（N），int（NJ））a+exp（E，EJ）a+int n（intN+intN）关系运算符的工作原理与算术运算符相同，除了我们对结果应用关系运算并返回布尔值：exp（E EJ）val（int（N），int（NJ））a0时，b[i]：= x %2;x：=x /2;i：=i +1odj：= i -1;whilej>= 0 dowriteb[j];j：=j -1奥德恩德函数main（void）beginwriteBinary（read）端public void run（0）;function f（1）{alloc（1）;alloc（32）;alloc（1）;l（i（1））：= i（0）;whilei（0）> i（0）do {l（l（i（1））+i（1））：=l（i（0）） %i（2）;l（i（0））：= l（i（0））/i（2）;l（i（1））：= l（i（1））+i（1）}的情况;l（i（34））：= l（i（1））- i（1）;while l（i（34））>=i（0）do{ writeInt（l（i（34））+i（1）;l（i（34））：= l（i（34））-i（1）}}public void run（0）{（1）函数类型}图三.源程序和翻译程序M. Hills等人/理论计算机科学电子笔记176（2007）215229程序K到MaudeK到CBCCJava烫发（6）80.8400.0480.1550.0030.174烫发（9）*45.560154.0161.61511.342二进制（1，000）17.0370.0190.1000.0040.190二进制（1，000，000）*32.631209.9494.95555.782筛（10，000，000）*27.671-1.1993.591河内（23）*18.14086.4324.39457.761执行时间（秒）。-表示未执行测试，-表示测试超时。评价依据-在电话会议上形成 Pentiumpyruvate 4CPU2.00GHz，1GBRAM，gcc版本3.3.6，编译标记：-O3-march=pentium4 -pipe-fomit-frame-pointer见图4。 评价结果对于汉诺塔问题，运用递归函数。结果如图4所示。我们SILF的C解释器优于BC，与C竞争，偶尔优于Java（需要额外的工作来确定在什么情况下）。Maude正因为如此，对于较大的测试用例，我们没有Maude的数据。5相关工作有许多不同的方法来指定程序语言的语义，包括操作方法，如Plotkin的SOS [ 8 ]，表示[6] 和MSOS[7]，以及Meseguer和RoRansuK允许复杂的控制流，例如循环中断和继续，异常和调用/cc，这些都很难使用操作方法（如SOS或MSOS）来指定，但还没有为语言相关的证明开发相同的“工具集”，例如使用归纳技术（例如，用于主题归约）的SOS定义。 指称方法和K似乎为定义语言特征提供了类似的能力（至少在没有并发性的情况下），但可以说重写逻辑所涉及的数学比指称方法更简单，特别是那些使用范畴论的方法，如Moggi[5]。在语言语义的可执行定义方面也有重要的工作，包括前面提到的重写逻辑语义。另一个有趣的例子是Centaur [2]，它包括一个Prolog引擎，用于执行正式语言规范。我们相信重写引擎的高性能本质为运行解释器提供了一个更现实的平台，尽管我们还没有进行具体的性能比较。另一个可执行的语义框架是ASF+SDF [11]，它也使用术语重写来定义编程语言，但我们的上下文，基于延续的方法，涉及显式访问控制状态，似乎非常不同。重写逻辑语义的一个吸引人的方面是，230M. Hills等人/理论计算机科学电子笔记176（2007）215重写语言的逻辑定义给出了代数指称语义（初始模型语义）和操作语义（初始模型是可执行的）。在上述工作中，我们的工作与重写逻辑语义最相似;更准确地说，我们的框架可以被视为特定于领域的语法糖化重写逻辑语义框架（即去糖化将为我们提供语言语义的标准重写逻辑表示重写逻辑一个自然出现的问题是，使用K的语言定义与直接在重写逻辑中给出的语言定义有何不同。我们认为K提供了几个明显的优势。• 在我们使用重写逻辑来定义语言的经验中，我们注意到长规则，特别是那些具有复杂嵌套控制结构的规则，可能非常难以阅读。这给那些想用重写逻辑来定义语言但又发现它太复杂的人造成了障碍。 的紧凑性我们认为K规则大大提高了可读性;• 我们还注意到，对于长规则，无论是在最初编写规则时还是在后来修改规则时，都更容易犯错误。同样，K规则的简短性，特别是它既能省略不可信的上下文，又能只列出一次术语中未改变的部分，有助于缓解这个问题;• 如前所述，变量定义通常占模块的很大比例。推断变量种类的能力使定义更短，同时仍然允许显式排序注释用于文档目的;• 省略规则不需要的上下文部分的能力允许上下文，特别是规则中没有提到的那些部分，改变。这增加了规则的模块性，因为添加新的特征很少需要改变现有的规则。6结论和今后的工作在本文中，我们介绍了K语言定义框架，并使用它来定义一个简单的命令式语言。我们还展示了一个将这个定义翻译成C语言解释器的例子基于目前令人鼓舞的结果，我们相信这是一种很有前途的策略，可以从语言语义的定义中自 动 导 出解释器。今后还有许多工作要做。我们仍在寻找改进K的方法，因为我们获得了更多使用它来定义语言的经验我们还在继续研究在重写逻辑和C fromK定义时自动生成解释器的工作我们认为，没有理由不能以全自动的方式做到这一点。与此同时，我们正在寻找更精确地定义语言的语法和语义的方法，以允许自动生成语言解析器和其他静态工具，这些工具使用我们在K中定义的规则来处理程序文本。最后，我们要感谢匿名审稿人的宝贵反馈，这使我们能够提高本文的质量M. Hills等人/理论计算机科学电子笔记1