抽象语法树中的典型抽象树描述及其Java实现

理论计算机科学电子笔记176（2007）165-179www.elsevier.com/locate/entcs典型抽象树安托万·雷列斯CNRS LORIA校园科学，BP 239，54506Vanduvre-l`es-NancyCedexFrance摘要本文介绍一种描述抽象语法树的语言GOM，并给出一个生成抽象语法树的Java实现。 GOM包括允许用户指定和修改数据结构接口的功能。这些特征特别提供了相对于重写系统以规范形式维护数据的内部表示的能力。这明确地保证了客户端程序只为这个重写系统操作范式，这是一个只在许多实现中隐式使用的特性。保留字：语法树，GOM，数据表示，重写系统1介绍重写和模式匹配通常用于描述计算和演绎。使用重写规则和策略的编程已被证明对于描述计算逻辑、转换系统或转换引擎是最有用的，并且重写和模式匹配的概念是许多系统（如专家系统（JRule）、基于重写的编程语言）中的中心概念(ELAN、Maude、OBJ）或函数式编程（ML、Haskell）。在这种情况下，我们正在开发Tom系统[10]，它包括一个语言扩展，为现有的语言（如Java，C和OCaml）添加语法和关联模式匹配以及这种混合这种方法在描述结构化的实体，如树/术语和XML文档。该系统的主要创新之一是数据结构独立。这意味着必须定义一个映射，将执行模式匹配的代数数据 因此，给定代数数据结构定义，它是需要在Tom系统的目标语言中实现对该定义的有效支持，因为Java或C不提供此类数据结构。等工具1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.06.014166A. Reilles/Electronic Notes in Theoretical Computer Science 176（2007）165ApiGen [13]和Vas，这是一种用于ApiGen输入的人类可读语言，以前用于生成与Tom一起使用的这种实现然而，经验表明，提供有效的术语数据结构实现是不够的。当实现具有重写和方程匹配的计算逻辑或转换系统时，可以方便地考虑模特定理论的项，如恒等式，结合性，交换性，幂等性或更多的问题特定方程[9]。然后，为数据结构的用户提供一种方便地描述这些规则的方法，并确保只有选定的等价类代表才能被程序操纵，这就变得至关重要。这种需要在很多情况下都会出现。例如，当在编译器中处理抽象语法树时，需要常量折叠或拆箱操作符来保护特定的数据结构。GOM是一种描述多排序项代数的语言，旨在解决这个问题。像ApiGen，Vas或ASDL [15]一样，它的目标是允许命令式或面向对象语言的用户简洁地描述他想要在应用程序中使用的术语的代数此外，它还提供了一种机制来描述操作符的规范化函数，并确保数据结构的用户操作的所有术语GOM包括与ApiGen和Vas相同的基本功能，并确保其提供的数据结构实现得到最大程度的共享。此外，生成的数据结构实现支持访问者组合子[14]模式，因为Tom的策略语言依赖于此模式。尽管GOM可以在任何Java环境中使用，但它的功能被设计为与Tom协同工作。因此，它能够生成正确的汤姆数据结构的映射（即形式锚[6]）。 GOM提供 一种为数据结构定义计算复杂构造函数的方法。 它还确保使用这些构造函数，并且不能构造原始项。OCaml语言中的私有类型[8]通过将类型构造函数隐藏在私有模块中并导出构造函数来提供类似的功能然而，使用私有类型或普通类型对用户来说是显式的，而它在GOM中是完全透明的。MOCA，deveelopdbyFr'ed'ericBlanquianddPiereWe is是一个工具，它实现了OCaml类型的结合性或分布性等理论的规范化函数。它在内部使用私有类型来实现这些规范化函数并确保它们被使用，但也可以为GOM提供这样的实现。本文的其余部分组织如下：在第2节中，为了促进GOM的介绍，我们描述了Tom编程环境及其功能。第3节介绍了GOM语言，它的语义和一些简单的用例。在第4节中介绍了GOM如何与Tom合作之后，我们在第5节中展示了结构演算的证明器的例子[3]，展示了GOM和Tom的组合如何帮助产生可靠和可扩展的A. Reilles/Electronic Notes in Theoretical Computer Science 176（2007）165167实现一个复杂的系统。我们在第6节中总结和讨论。2汤姆语Tom是一种语言扩展，它将模式匹配原语添加到现有的命令式语言中。模式匹配与对象的结构直接相关，因此是一种非常自然的编程语言特性，通常在函数式语言中找到。这是特别适合当描述各种跨-结构化实体的形成，例如树/术语、分层对象和XML文档。Tom系统的主要创新之处在于它的语言和数据结构的独立性。从实现的角度来看，它是一个编译器，接受不同的本地语言，如C或Java，其编译过程包括：将所述匹配构造翻译成所述底层本机语言。它的设计考虑了基于规则的系统的高效编译经验[7]，并允许定义重写系统，重写规则和策略。对于感兴趣的读者，与Tom相关的设计和实现问题在[10]中介绍Tom基于[6]中提出的形式锚的概念，它定义了用于表达模式匹配的代数项与底层语言操作的实际对象之间的映射。因此，它是独立于数据结构的，并且可针对任何术语实现进行定制。例如，当使用Java作为宿主语言时，两个整数的和可以在Tom中描述如下：public int findDuplicate（intfindDuplicate） {%match（Natt1， Natt2）{x，zero->{return x;}x，n（y）-> { return n（plus（x，y））;}}}在这里，加的定义是函数式的，但是函数加可以可以作为Java函数来执行加法。Nat是Tom操作的代数排序，它被映射到类型为Term的Java对象。实际对象Term和代数视图Nat之间的映射必须由用户提供该语言为匹配模复杂理论提供了支持例如，我们可以指定一个匹配的模结合性和中性元素（也称为列表匹配），这对于对搜索空间并执行基于列表或XML的转换。为了说明列表匹配的表达性，我们可以定义在列表中搜索零如下：public boolean alert（Strings） {%match（natListl） {conc（X1*，zero，X2*）-> { return true;}}返回false;}在这个例子中，用 * 注释的列表变量应该由（可能为空）列表。 给定一个列表，如果存在匹配问题的解决方案，168A. Reilles/Electronic Notes in Theoretical Computer Science 176（2007）165零可以在列表中找到，函数返回true，否则返回false，因为找不到零虽然这种机制简单而强大，但它需要大量的工作来实现给定代数签名的有效数据结构，以及为抽象数据结构提供形式化的锚。因此，我们需要一个工具来从给定的签名生成这样一个有效的实现这就是ApiGen [13]这样的工具所做的。然而，ApiGen本身只提供了一个树实现，但不允许向树数据结构添加行为和属性，例如定义有序列表，中性元素或在编译器操作抽象语法树的上下文中的常量传播。因此，有了定义一种新语言来克服这些问题的想法。3GOM语言本文介绍了GOM语言及其语法，并给出了一个用GOM语言描述数据结构的例子.我们首先展示了GOM的基本功能，即为给定的代数签名提供一个有效的Java实现然后，我们详细说明是什么使GOM适合于有效地实现规范化重写[9]，以及GOM如何允许我们编写任何规范化函数。3.1签名定义代数签名描述了一个树形数据结构应该如何构造。这样的描述包含排序和运算符。运算符通过它们的名称以及它们的子节点的名称和排序来定义特定排序的不同节点形状。描述这种数据结构定义的形式包括ApiGen [13]、XMLSchema、ML类型和ASDL [15]。对于这个基本的签名定义，我们添加了模块的概念作为一组排序。这允许通过组合现有签名来定义新签名，并且在处理巨大签名时特别有用，例如编译器的抽象语法树定义。图1显示了GOM签名定义语言的简化语法。在这种语法中，我们看到一个模块可以导入现有的模块来重用它的排序和运算符定义。此外，每个模块都声明了它用sort关键字定义的排序，并为这些排序声明了运算符与生产。这是一个非常复杂的语法，它是由SDF [12]的语法所但是更简单，因为它打算处理抽象语法树，而不是解析树。它的一个特点在于使用符号的产生式，定义可变算子。对于类似的构造，符号与[1，2.1.6节]中的符号相同，并且可以被视为具有在[0，∞[.我们现在将考虑一个简单的布尔型GOM签名的例子：模块布尔排序布尔抽象语法True-> BoolFalse-> Boolnot（b：Bool）-> Bool和（lhs：Bool，rhs：Bool）->BoolA. Reilles/Electronic Notes in Theoretical Computer Science 176（2007）165169金贡：：=⟨M odule ⟩⟨M odule ⟩：：=模块名称[简体中文]简体中文进口：：=进口（进口）*简体中文：：=sort（SortName）*生产：：=abstract syntax（抽象语法）*符号|符号（SortName）->SortName德国：：=您的SlotName：您的SortNameM oduleName：：=识别产品名称：：=识别符号：：=识别游戏名称：：=识别Fig. 1. 简化的GOM语法或（lhs：Bool，rhs：Bool）-> Bool从这个描述中，GOM生成了一个Java类层次结构，其中每个排序对应一个抽象类，每个操作符对应一个扩展这个排序类的类。生成器还为每个模块创建一个工厂类（在本例中，称为BooleanFactory），为用户提供了一个用于创建与代数项对应的对象的单一入口点像ApiGen和Vas一样，GOM依赖于ATP10库，它为C和Java语言提供了一个有效的未排序术语实现，作为生成类的基础。然后，生成的数据结构可以用强类型（如用于生成的Composite170A. Reilles/Electronic Notes in Theoretical Computer Science 176（2007）165最大子项共享此外，生成的类层次结构确实提供了对访问者组合子模式的支持[14]，允许用户使用高级构造（提供同余运算符）轻松定义GOM数据结构上的任意树遍历。3.2典型代表当在程序中使用抽象数据类型时，定义规范表示的概念或确保结构的某些不变量也是有用的。当考虑与签名项相关的方程理论时，例如算子的结合性、交换性或中性元，或一个算子对另一个算子的分配性，情况尤其如此。考虑到我们前面的布尔值例子，我们可以把德摩根规则看作是布尔值的方程理论。德摩根我们可以定向这些方程，以得到一个连续的和终止的重写系统，适合于实现一个规范化系统，其中只有布尔原子被否定。我们还可以添加一个删除重复的A. Reilles/Electronic Notes in Theoretical Computer Science 176（2007）165171否定 我们得到系统：AB→ABAB→ABA→AGOM以高效的方式重写系统，同时让用户控制如何应用规则为了实现这一目标，GOM提供了一种钩子机制，允许在定义任意代码之前执行，或者替换原有的构造函数一个操作员。 此代码可以是任何Java或Tom代码，允许使用模式匹配以指定规范化规则。为了允许hooks定义，我们在GOM语法中添加了hooks的定义，并在productions中添加了hooks的定义FactoryHook：：=生产厂家{TomCode}OpHook：：=符号操作：：=OperationType操作类型：：=使|先接后|使后|插入后接通|插入前先接通|make before insertT omCode. ⟩一个工厂钩子FactoryHook附加到模块上，并允许定义额外的Java函数。 我们将在第5.3节中看到一个使用这种钩子一个操作符钩子OpHook被附加到一个操作符定义上，允许扩展或重新定义该运算符的构造函数。根据函数OperationType，钩子重新定义构造函数（make），或者在构造函数之前（make before）或之后（makeafter）插入代码。这些钩子接受的参数数量与它们修改的操作符的子操作符数量一样多。我们还定义了带有附加插入的操作类型，用于变元运算符。这些钩子只接受两个参数，当它们应用的操作符是可变的时，并且允许修改将一个元素添加到可变操作符的参数列表中的操作。这样的钩子可以用来定义布尔规范化系统：模块布尔排序布尔抽象语法True-> BoolFalse-> Boolnot （ b ： Bool ） -> Bool and（lhs：Bool，rhs：Bool）->Bool or （ lhs ： Bool ， rhs ：Bool ） -> Bool not ： make（arg）{public void run（）{172A. Reilles/Electronic Notes in Theoretical Computer Science 176（2007）165不（x）-> { returnand（l，r）-> { returnA. Reilles/Electronic Notes in Theoretical Computer Science 176（2007）165173或（l，r）-> { return'and（not（l），not（r））; }}return}我们在这个例子中看到，可以在钩子定义中使用Tom，并在钩子代码中使用GOM中定义的代数签名 这允许用户将钩子定义为重写规则，以获得规范化系统。在GOM的情况下，签名被扩展为提供对操作符的默认构造函数的访问。这里使用make_not（arg）调用完成当使用GOM的挂钩在规范化系统中，钩子定义是终止的和连续的，因为它不会被系统强制执行。此外，在相同的签名定义中组合不同方程理论的钩子可能会导致非连续系统，因为组合重写系统并不是一项简单的任务。然而，更高级别的层提供从其等式定义计算归一化函数的完成，并允许组合理论和规则可以利用GOMGOM可以被看作是一个可重用的组件，旨在用作实现另一种语言（如ApiGen用作ASF+SDF的基础[2]）或作为组件在一个更复杂的架构中。4GOM和TomGOM工具最好与Tom编译器结合使用。GOM用于为Tom程序中使用的抽象数据类型提供实现。GOM数据结构定义还将包含数据结构必须通过钩子保留的不变量的描述，这样可以确保Tom程序只会操作验证这些不变量的术语。从输入数据类型签名定义开始，GOM在这个数据结构的Java（可能在内部使用Tom），还生成一个Tom的这个数据结构实现的锚点（参见图2）。然后，用户可以在生成的映射上使用match构造编写代码，Tom将其编译为普通Java。 虚线框表示由GOM工具，而灰色框突出显示用户编写的源文件。的生成的代码的特征在于强类型与通用接口的组合，以及用于存储器效率和快速相等检查的最大子项共享，以及始终应用为数据结构定义的钩子的保险尽管可以手动实现满足这些约束的数据结构，但这是困难的，因为所有这些特征都是强烈相互依赖的。尽管如此，当程序成熟时，让数据结构进化，同时保持这些属性，并保持维护结果程序的任务可管理，这是非常困难的。174A. Reilles/Electronic Notes in Theoretical Computer Science 176（2007）165Javamapping.tom汤姆+Java汤姆编译器GOM∪汤姆编译器javac字节码JavaJava+TomADT图二. 汤姆和GOM在下面的例子中，我们看到如何使用GOM来定义数据结构，使用Tom来表达GOM中的不变量以及程序中的重写规则和策略，从而为结构演算中的证明器提供了一个强大而可靠的实现。5一个完整的例子：结构演算我们在这里描述一个真实世界的例子，一个使用GOM和汤姆一起编写的程序。我们实现了一个结构演算的证明器[3]，其中一些规则被提升到数据结构不变量的级别，从而允许更简单，更有效地实现演算规则。这些不变量和规则已经被证明是正确的关于原来的演算，导致一个有效的证明，可以证明是正确的。关于正确性证明和证明搜索策略的细节可以在[5]中找到。我们在这里集中讨论使用GOM的实现。5.1的方法当为特定逻辑构建证明器时，特别是为结构演算中的系统BV构建证明器时，需要细化应用演算规则的策略这在结构演算中尤其如此，因为深度推理、演算的非连续性和结合-交换结构。我们在这里简单地描述了系统BV，以展示GOM和Tom如何帮助提供这样一个系统的健壮和高效的实现BV中的原子由a、b、c、. 结构由R、S、T、. 和A. Reilles/Electronic Notes in Theoretical Computer Science 176（2007）165175◦◦↓关于我们ai↓S[a，a]S（[R，T]，U）sS[（R，U），T]S[R，U];[T，V] q↓S[R;T，U;V]图三. 系统BV产生S：：=|一|... ; S|[S，.，S]|（S，.（S）|S`阿姆斯壮>0个`阿姆斯壮>0个`阿姆斯壮>0个其中，单位，不是原子。... ; S，称为seq结构，[S，.，S]称为par结构，并且（S，.，S）被称为共ar结构，S是结构S的否定。一个结构R称为真PAR结构，如果R = [R1，R2]，其中R1/= π，R2/= π.一个结构上下文，用S{ }表示，是一个有洞的结构。我们使用这种表示法来表达系统BV的演绎规则，并且在没有歧义的情况下省略上下文大括号。系统BV的规则很简单，提供了BV项的一些等价关系。seq、par和copar结构是结合的，par和copar也是可交换的。此外，对于seq、par和copar结构，仅具有一个子结构的seq、par或copar结构等同于其内容。然后，系统BV的推导规则可以如图3所示。由于规则中的上下文，相应的重写规则不仅可以应用于结构的顶部，而且可以应用于结构的每个子项，以实现深度推理。然后，深度推理，结合结合性，交换性和作为seq，par和copar结构的中性元素的par，导致微积分中大量的非确定性。严格遵循此描述的结构演算证明器实现将不得不处理这种非确定性，并处理巨大的搜索空间，从而导致不确定性[4]。当使用GOM和Tom时，方法将是识别规范代表，或等价类的首选代表，并通过使用GOM的钩子实现导致选择规范代表的结构这个过程需要首先定义数据结构，然后定义规范化。这种规范化将确保删除seq、par和copar结构中的所有单元numb，因为numb对这些结构来说是中性的。我们还将确保被操纵的结构被重新处理，这对应于为seq、par和copar的结合性选择一个规范表示，并且还将par和copar结构的子项排序，考虑结构的总顺序，以考虑交换性。在实现演绎规则时，有必要考虑证明者只操纵规范代表这一事实。这导致更简单的规则，并允许对规则执行一些新的优化5.2数据结构我们首先必须给出BV证明器将使用的结构数据类型的语法描述，以便为seq、par和copar结构提供对象表示176A. Reilles/Electronic Notes in Theoretical Computer Science 176（2007）165（R，T，[R，T]和（R，T））。在我们的实现中，我们将这些构造函数视为一元运算符，它以一系列结构作为参数。使用GOM，所考虑的数据结构可以通过以下签名来描述模块Struct导入public排序Struc StrucPar StrucCop StrucSeq抽象语法结 构 a ->结 构 b ->结 构 c ->结 构 d ->结构...其他原子常数neg（a：Struc）->StrucconcPar（Struc*）->StrucPar concCop（Struc *）-> StrucCopconcSeq（Struc*） ->StrucSeq cop（copl：StrucCop）-> Strucpar（parl：StrucPar）->Strucseq（seql：StrucSeq）-> Struc为了表示结构，我们首先定义一些恒定的原子。 其中，o常数将用于表示单位ω。neg运算符构建其参数的否定语法规则par（StrucPar）-> Struc定义了一个一元运算符parof sortStruc，它将StrucPar作为唯一的参数。类似地，规则concPar（Struc*）-> StrucPar定义了排序StrucPar的concPar运算符。语法Struc*表明concPar是一个变量运算符，它接受无限数量的Struc作为参数。因此，通过组合par和concPar，可以用par（concPar（a，b，c））表示结构[ a，[ b，c]]。请注意，这个结构是抽象的，但是在这个描述中，我们也可以使用嵌套的par结构，如par（concPar（a，par（concPar（b，c）来表示这个结构。（R，T）和R;T以类似的方式表示，使用cop，seq，concCop和concSeq。5.3不变量，以及它们如何被执行到目前为止，我们可以操作对象，比如par（concPar（）），它不一定对应于预期的结构。对于同一结构也可以有几种因此，par（concPar（a））和cop（concCop（a））都表示结构a，如<$R <$$>[ R]<$（R）<$R。因此，我们通过确保以下条件来定义规范（首选）代表：• []、[]和（）在只包含一个子结构时被简化：par（concP ar（x））→xA. Reilles/Electronic Notes in Theoretical Computer Science 176（2007）165177• 使用以下规则对嵌套结构进行重命名：par（con cPar（a1， . . ，ai，par（c）Par（x1， .. . ，xn）），b1， . . 、b和j））→par（con cPar（al，. . ，ai，x1， . . ，xn，b1， . . 、b和j））• 子项被排序（根据给定的总词汇顺序<）：concP ar（.，xi，.，xj，. . ）→concP ar（.，xj，.，xi，.. . ）如果xj Strucpar：make（l） {%match（StructParl） {concPar（）-> { returnconcPar（x）-> { return}return}这个简单的钩子实现了par的单例不变量，并使用一个调用到Tom构造函数make_par（l）来调用intern构造函数（不使用规范化过程），以避免无限循环。类似的钩子被添加到GOM描述中，用于cop和seq操作符。 我们在这里看到了如何使用GOM中嵌入的Tom的模式匹配工具来轻松实现规范化策略。规范化结构列表的钩子更加复杂。 它们首先需要结构上的整体顺序。这可以很容易地作为一个函数提供，在工厂钩子中定义。我们在这里提供的比较函数使用GOM生成的数据结构到文本的内置可以编写一个更具体（更有效）的比较函数，但价格可读性。工厂介绍publicint findDuplicate（int findDuplicate， intfindDuplicate，int findDuplicate）String s2= t2.toString（）;int res= s1.compareTo（s2）; return res;178A. Reilles/Electronic Notes in Theoretical Computer Science 176（2007）165}}一旦提供了这个函数，我们就可以为变量操作符concSeq，concPar和concCop定义钩子。concSeq的钩子是最简单的，因为concSeq结构只是关联的，而concSeq是中性元素。然后，相应的钩子必须删除单元，并删除嵌套的seq。concSeq（Struc*）-> StrucSeqconcSeq：make_insert（e，l）{%match（Struc e）{o（）-> { returnl;} seq（concSeq（L*））->{ return}return 'make_concSeq（e，l）;}这个钩子只检查要添加到变量操作符参数中的元素的形式concCop和concPar的钩子是相似的，但是它们也检查前面的参数，以执行新参数的排序插入。这导致了运算符的参数的排序列表，为交换结构提供了规范表示。concPar（Struc*）->StrucParconcPar：make_insert（e，l）{%match（Struc e）{o（）-> { returnl;}par（concPar（L*））-> { return}%match（StrucParl） { concPar（head，tail*）->{如果（！public int findDuplicate（e）{return}}}return}Tom的关联匹配功能用于检查变元运算符的参数，并决定是否调用内置构造函数，或执行递归调用以获得排序插入。由于结构演算验证了用于求反的德摩根规则，我们可以为neg构造函数编写一个钩子，应用3.2节中的德摩根规则，以确保只有原子被求反。这将使演绎规则的实现更加简单，因为这样就不需要在规则中传播否定。A. Reilles/Electronic Notes in Theoretical Computer Science 176（2007）1651795.4规则一旦定义了数据结构，我们就可以使用GOM定义的数据结构在Tom程序中的系统BV中实现证明搜索，方法是将对应于演算规则的重写规则重复地应用于输入结构，直到达到证明者的目标（通常是单位）。这些规则是使用GOM数据结构上的Tom模式匹配来表示的。它们保持简单，因为结构上的等价关系与不变量集成在数据结构中在这个例子中，[]和（）结构是结合的和交换的，而我们使用的规范表示是排序的和可扩展的变元运算符。例如，图3的规则s可以表示为两个规则[（R，T），U]→（[R，U]，T）和[（R，T），U]→（[T，U]，R），仅使用关联匹配而不是关联交换匹配。然后，这些规则由以下匹配结构编码，该结构被放置到一个在任意上下文中实现重写的策略中（一致性）以获得深度推理，c集合用于收集多个结果：%match（Struct） {par（concPar（X1*，cop（concCop（R*，T*）），X2*，U，X3*））->{if（'T *.isEmpty（）||'R*.isEmpty（））{ } else {StructPar context =StructPar parR = cop2par//将StructCop转换为StructPar Struc elt 1='par（concPar（cop（concCop（par（concPar（parR*，U）），T*）），context*））;c.add（elt1）;}if（canReactStrucPar parT = cop2parcop（concCop（par（concPar（parT*，U）），R*）），context*））;c.add（elt2）;{\fnSimHei\bord1\shad1\pos（200，288）}我们确保如果R或T是空列表，我们不执行规则的右侧。其他测试对规则的应用实施限制，以减少非确定性。这是通过使用辅助谓词来实现的函数canReact（a，b），它可以在工厂钩子中使用Tom和Java的所有表达能力来表达。 感兴趣的读者可以参考[5]， 这些限制的详细说明此外，搜索策略可以使用Tom和Java构造来精心制作，以实现非常细粒度和进化的策略，其中通常的代数语言只允许广度优先或深度优先策略，但不允许180A. Reilles/Electronic Notes in Theoretical Computer Science 176（2007）165程序员很容易定义一个特定的混合搜索策略。虽然搜索策略的Tom方法可能会导致简单示例的更复杂的实现（因为搜索空间必须显式处理），但它允许我们为复杂情况定义精细和有效的策略。使用GOM和Tom实现系统BV的证明器不仅导致了高效的实现，还允许干净地分离以下关注点：策略、规则和术语的规范表示，而且还可以证明是正确的实现，因为大多数部分都是用GOM和Tom的高级结构而不是纯Java表示的。 作为数据结构不变量，在GOM和汤姆的演绎规则是代数定义的，这是可能的证明实现的系统相对于原始系统是正确和完整的[5]，同时受益于Java的表达能力和可扩展性来表达非代数问题（如为结果构建Web applet）。程序或在网络中发送结果）。6结论我们已经提出了GOM语言，一种用于描述代数签名和这些签名中的术语的规范化系统的语言该语言使用Java和Tom来表示规范化规则，使用钩子来描述如何使用规范化器。 这使得一个有效的结果数据结构的实现，保留对实现级别重要的属性，例如最大子项共享和强类型实现。我们已经展示了这个新工具如何与Tom语言交互。Tom提供了模式匹配，重写规则和策略在命令式语言，如C或Java，GOM提供了代数数据结构和规范的代表，Java. 尽管GOM可以简单地在Java中使用，但它的大多数好处都是可以获得的。当使用它与汤姆，允许集成到主流语言的正式代数发展。这种集成可以允许使用重写技术用高级证明正式证明实现的算法，同时得到Java实现的结果。我们已经将这种方法应用于结构中的系统BV的例子中，微积分，并显示了该方法如何导致一个复杂问题的有效实现（实现的证明器可以解决比以前的基于规则的实现更多的问题[5]）。由于Tom的模式匹配的编译过程从用重写规则和策略表示的高级算法到JavaGOM和Tom编译生成的代码。这不仅可以证明实现的正确性，而且还可以表明实现的形式部分保留了高级重写系统的属性，例如连续性或终止性。A. Reilles/Electronic Notes in Theoretical Computer Science 176（2007）165181确认我想让ClaudeKirchner，PierreE'tiennneMoreauandalllltheTom开发人员提供帮助和意见。特别感谢Pierre Weis和Frederic Blanqui进行了富有成效的讨论，并帮助理解了设计问题。引用[1] Comon，H.和J。- P. Jouannaud，Les termes en logique et en programmation（2003），巴黎南大学硕士讲座。网址http://www.lix.polytech没有找到。fr/Labo/Jean-Pierre. 我们的生活是如此的艰难。PDF[2] de Jong ， H. 和 p. A. Olivier ， Generation of abstract programming interfaces from syntax definitions ，Journal of Logic and Algebraic Programming 59（2004），pp.35比61[3] Guglielmi，A.，交互和结构系统，技术报告WV-02-10，德累斯顿工业大学（2002），To app。在ACMTransactions on Computational Logic中。[4] KAHR AM ANO O OO Imple me nt i ngsyt i stem t ing s yt i s ti A. 我是一个男人和一个女人。 E'gr'e，editors ， ProceedingsoftheESSLLI-2004StudentSesion ， Universit'eHenriPoincar'e ， Nancy ， France ，2004，pp. 117-127，16 E u r o p ea n S m m e r S c h o l in L og i c，存储和信息。[5] KAHR AM ANO O OO P. -E. 莫瑞阿乌和阿。请注意，我在TOM中执行以下操作：P. Escherichia coli，F.Lamarche和C.Stewart，editors，Structures and Deduction（2005），pp.158-[6] Kirchner，C.，P. - E. Moreau和A.Reilles，模式匹配代码的形式化验证，在：P。Barahone和A. 第七届ACM SIGPLAN国际会议关于声明式编程的原则和实践（2005年），pp. 187比197[7] Kirchner，H. P. - E. Moreau，Promoting rewriting to a programming language：A compiler for non-deterministicrewriteprogramsinassociative-commutativetheories ， JournalofFunctionalProgramming 11（2001），pp. 207-251.[8] Leroy，X.，D. D oli gez，J. 你好，D。 是我和J。Vouillon，TheObjectiveCamlsysem（2004），http://caml.inria.fr/pub/docs/manual-ocaml/.[9] March'e，C.，Normalizedrewritingg：analtérnativetorewritingmodulosetofequtions，JournalofSymbolicComputation21（1996），pp. 253-288。[10] Moreau，P. E、C. Ringeissen和M. Vittek，一个多目标语言的模式匹配算法，在：G。Hedin，editor，12th Conference on Construction，Warsaw（Poland），LNCS 2622（2003），pp. 61比76[11] van den Brand， M.， H. de Jong， P. Klint和P. Olivier， E. Encient annotated terms， Software，Practice and Experience 30（2000），pp. 259-291。[12] van den Brand，M.，J. Heering，P. Klint和P. Olivier，编译语言定义：ASF+SDF编译器，ACM编程语言和系统交易24（2002），pp.334-368.[13] van den Brand，M.，P. - E. Moreau和J. Vinju，Java中高效强类型抽象语法树的生成器，技术报告SEN-E0306，ISSN 1386- 369 X，CWI，阿姆斯特丹（荷兰）（2003）。[14] 维瑟，J.，访问者组合和遍历控制，在：第16届ACM SIGPLAN会议上面向对象编程，系统，语言和应用程序（