Maude 2.0：通用性、性能和互联网编程的增强

理论计算机科学电子笔记36（2000）网址：http://www.elsevier.nl/locate/entcs/volume36.html22页走向莫德2.0*M. Cl avela，F. Dur'anb，S. Ekerc，P. Lincolnc，N. Mart's-Olietd，J. Meseguerc和J. F.克萨达eaDep artamentodeFilosof'ıa，UniversidaddeNavarra，SpainbETSII，UniversidaddeMa'laga，西班牙cSRI International，Menlo Park，California，USAdFacultaddeMatema'ticas，孔普鲁腾塞大学，马德里，西班牙eCentrodeInforma'ticaCient'fiacadeAndaluc'ıa，Sevilla，Spain摘要Maude 2.0是目前正在开发的Maude重写逻辑语言的新版本。Maude 2.0的三个主要目标是：（i）更大的通用性和表现力;（ii）对更广泛的编程应用程序的有效支持;以及(iii)可用性是开发互联网编程和移动计算系统的关键组成部分。为了实现这些目标，增加了一些新功能。功能模块的隶属关系方程逻辑和系统模块的重写逻辑现在支持在其最大可能的通用性，和面向对象的模块的操作语义保证对象和消息的公平性。由于参数化的理论和视图，Full Maude中的模块操作也更加通用。Maude编译器（在667MHz的Xeon上每秒可重写1500万次）和新的内置模块库都为更广泛的编程应用提供了有效的支持。除了新的内置功能模块，一个关键的新功能是内置的面向对象模块，提供与外部对象（如文件系统，窗口系统和互联网套接字）的灵活交互。特别是，内置的互联网套接字将提供良好的支持，一个新的声明式风格的互联网编程在Maude，并将被用作一个关键的构建块，以实现移动Maude语言。*由DARPA通过罗马实验室合同F30602-97-C-0312提供支持，由O.海军研究合同N 00014 -99-C-0198，并由国家科学基金会资助CCR-9505960和CCR-9900334。2000年由ElsevierScienceB出版。 诉 操作访问和C CB Y-NC-ND许可证。C LAVELet al.21介绍Maude 2.0是目前正在开发的Maude的新版本。本文介绍了我们的详细设计的Maude 2.0的主要功能，其中一些已经实现。Maude 2.0本文解释了我们在支持这三个主要目标的设计决策。第2节重点介绍新的模块语法和语义，支持更大的通用性和规范的表达能力。从本质上讲，underlying逻辑成员资格方程逻辑的功能模块，和重写逻辑的版本扩展它的系统模块，将支持在其最大可能的一般性。类似地，参数化模块、理论和视图将通过参数化理论和参数化视图支持更大程度的模块化和可重用性。所有模块的操作语义也将得到扩展。特别是，额外的变量将被允许在条件中，对于条件规则，可能包括重写条件;此外，面向对象的模块将由规则的默认解释器以对象和消息公平的方式执行对许多编程应用程序的有效支持需要足够的内置模块库和高级编译技术。这两个主题分别在第3节和第6节中讨论。除了一些新的内置功能模块，其中最重要的是字符串，一个关键的新颖性是增加了内置的面向对象的模块。这些模块将与普通的面向对象模块无缝集成。通过这种方式，普通的Maude对象将能够通过消息传递与内置对象（如文件系统，窗口系统和Internet套接字）进行通信和交互。这将极大地扩展可支持的应用程序的范围，并将为编程交互式应用程序提供更大的灵活性内置互联网套接字将是一个关键功能，允许使用Maude作为互联网编程语言，并将支持在Maude之上实现Mobile Maude语言[9]第6节解释了Maude编译器，它已经相当先进和高效，并且将与Maude 2.0解释器集成语言的任何变化和进步都必须在META-LEVEL模块中反映出来。第4节解释了如何做到这一点，同时在术语和模块的元表示中实现更大的简单性和经济性，并提供更丰富的元级操作集第5节中收集了其他两个杂项特性，即新的模块系统，它允许在涉及大型模块层次结构的规范中实现更大的效率，以及latex属性，它可以为模块中的任何运算符声明，以输出模块声明和求值表达式。C LAVELet al.3所需的LATEX数学符号。文章最后在第7节中得出了一些结论附录给出了一些关于一些内置模块的更多细节，并提供了一个基于内置Internet套接字的Internet编程应用程序示例本文假设读者对Maude的基本概念有一定的了解例如它在隶属方程逻辑[2]和重写逻辑[17]中的逻辑基础，它的功能模块、系统模块和面向对象模块，以及模块操作，以及它的相关特征，我们请读者参考[7，6]。2新的模块结构和语义本节讨论对函数式、系统和面向对象模块的当前语法和语义的扩展，以及Maude 2.0中将支持的参数化模块和理论的2.1功能模块函数模块的新语法扩展了以前的语法，以允许在支持成员关系方程逻辑规范方面实现最大可能的通用性首先，为了支持部分操作的指定，这些操作不限于对类的乘积的全函数，我们允许在类级别显式声明这样的在隶属方程逻辑中，有类而无类的项被理解为未定义项或错误项。一个种类k有一个相关联的排序族Sk，它们在语义上被理解为子集。一般来说，一个在种类层次上的全函数只限制于一个在排序层次上的部分在功能模块中，类型没有显式命名。相反，我们用其排序的集合Sk来识别一个种类k，将其理解为一个等价类模由子排序排序生成的等价关系，也就是说，两个排序在这个等价关系中当且仅当它们属于相同的连通这是一个集合中的元素。因此，对于任何s∈Sk，[s]表示kindk =Sk，被理解为各种偏序集的连通分量，属于S的。当一个模块被导入到另一个模块时，这提供了一种非常健壮的引用等价类的方法，这可能会增加类中的排序数量，甚至可能合并几个类。例如，如果在一个新模块中引入了一个前一个排序s的新超级排序sJ，那么，[s] 和[sJ]是指同一种类的两种等价方式例如，考虑图中路径的连接函数它实际上是一个局部函数。它可以在用户定义的超级分类路径上进行总计？但是在类的层次上通过声明来定义它会更简单、更优雅op _;_：[Path] [Path] -> [Path]。第二个语法扩展涉及变量的处理。可变C LAVELet al.4现在是一个标识符，由一个名称、一个冒号和一个排序或种类名称组成。例如，P：Path是一个排序Path的变量。通过这种方式，变量不必在变量声明中声明：它们可以直接出现在术语中。为方便起见，仍然允许使用变量声明，但声明vars P Q R S：Path.现在被理解为别名定义，例如，允许使用名称P作为变量P：Path的缩写。第三个语法扩展涉及条件方程和条件成员中的方程条件的处理这样的条件是方程和隶属度的连接，并且它们由单个方程t = tJ和隶属度t：s通过二元连接符/\（假设是关联的）组成。此外，条件中方程的具体语法有两种变体，即常方程t = t两者在数学语义上具有相同的等式解释，但操作语义不同，如下所述。例如，假设上面的变量声明，路径串联的结合性可以由条件方程表示如果t（P）=s（Q）/|t（Q）=s（R），则其中s和t分别是源函数和目标函数。请注意，不需要使用布尔值相等谓词==将条件表示为单个布尔条件。这仍然是可能的，即通过宣布当t（P）==s（Q）且t（Q）==s（R）时，但不是必需的。更一般地，布尔表达式b被允许在等式条件中作为合取词出现，作为等式b = true的简写。我们可以通过下面的函数模块PATH来说明上述扩展，对于图中的路径，它导入了一个模块A-GRAPH，该模块具有节点和边的排序，操作s和t，给出了每条边的源节点和目标节点，以及特定的边和节点常数，这些都不需要我们在这里关注（参见附录A.1中的示例然后，它根据以下等式和成员关系在这样的图上构建路径fmod PATH保护A-GRAPH。排序路径。子排序边<路径。op_;_：[Path] [Path] -> [Path]。ops st：Path -> Node。var E：边缘。 vars P Q R S：Path.cmb E; P：路径，如果t（E）= s（P）。ceq s（P）= s（E），如果E;S：= P。ceq t（P）= t（S），如果E; S：= P。如果t（P）=s（Q）/|t（Q）=s（R），则endfmC LAVELet al.5{←←}注意在定义源函数和目标函数的两个连续方程的条件下的匹配方程E;S：= P。如前所述，匹配方程在数学上被解释为普通方程;然而，在操作上，它们以特殊的方式被处理，并且它们必须满足特殊的要求。注意，上述匹配方程中的变量E和S并不出现在相应条件方程的左侧在这些方程的执行中，这些新变量通过将项E; S与绑定到变量P的主题项相匹配而被实例化。为了使这个匹配决定与绑定到P的基项相等，项E; S必须是一个模式。一般地，给定一个函数模M，我们称一个项t为M-模式，如果对于任何良构置换σ使得对于其定义域中的每个变量x，项σ（x）关于M中的方程是标准形的，则σ（t）也是标准形的。t是M-模式的一个充分条件是它的不变子项和M中方程的左边之间不存在单位元。在上面的例子中，多类单位元E P通过与结合方程的左侧统一而获得的Q，SR被成员资格P; Q： Edge不满足的事实排除。条件中的常方程t=tJ具有通常的运算解释，也就是说，对于给定的替换σ，σ（t）和σ（tJ）都被简化为标准形式，并比较等式，模在模块的运算符声明中指定的方程公理，如结合性，交换性和恒等式所有条件方程t = tJ，如果C1≥. Cn在功能模块M中，必须满足以下容许性要求1，确保所有额外变量将通过匹配而被实例化：(i)vars（T）vars（t）nj=1vars（C j）.(ii) 如果Ci是方程ui=uJi或隶属度ui：s，则i−1vars（Ci）vars（t）j=1vars（C j）.(iii) 如果Ci是匹配方程ui：=uJi，则ui是M-模式，i−1vars（uJi）vars（t）j=1vars（C j）.[1]这些要求包括[21]中所谓的适当定向和右稳定3-CTRS的特殊情况，当每个方程si=ti在其条件下表示为匹配方程ti：= si时。C LAVELet al.6从左到右依次尝试满足条件。由于匹配一般可以发生模方程公理，像往常一样，许多不同的匹配可能必须尝试，直到找到满足条件的所有变量的匹配尽管在条件中允许额外变量增加了一般性，但我们仍然期望函数模是Church-Rosser和[2，10.1节]意义上的终止代数方程逻辑规范。上述容许性要求和Church-Rosser假设和终止假设在支持逻辑的全部一般性的泛函理论中被放弃（见2.4节）。对于函数模块，Maude确实通过重写[2]中定义的操作语义来支持操作语义，并如[2]的第10.1节中所述一般化以允许额外的变量特别是，在Maude2.0中放弃了先前的严格性假设，即方程左侧的替换实例具有排序（参见[6，6.1节]），以允许更一般的非严格方程，例如用于错误恢复的方程。当需要严格性时，方程必须有确保严格性的显式条件。2.2系统模块在方程级，系统模块也支持所有的扩展，并满足已经为函数模块描述的相同的方程要求，包括方程是Church-Rosser的要求，并以给定的方程公理为模。此外，重写规则现在可以采用建立在隶属关系等式逻辑之上的重写逻辑的变体中的最一般的可能形式。也就是说，它们可以是以下形式：t→tJ 如果（我i=i（J2016 -05 -2200：01：01Kpk→qk）而不限制哪些新变量可以出现在右侧或条件中。也就是说，规则中的条件也由关联连接符I形成，但是它们通过还允许重写表达式来概括等式和成员关系中的条件，为此使用具体语法t=>t此外，方程、成员资格和重写可以以任何顺序混合，并且对于功能模块，条件中的一些最后，尽管条件重写规则具有完全的通用性，但我们仍然期望重写规则相对于模块中的方程是一致的或弱一致的[23]，以便推导的方程和重写部分可以有效地模块化。当然，在完全的一般性中，系统模块的执行将需要在元级别控制条件和右侧中额外变量的实例化的策略[3，22]。然而，一个非常通用的系统模块类，称为可接受模块，将由Maude 2.0如前所述，等式C LAVELet al.7EE系统模块的一部分必须始终满足第2.1节中对功能模块的相同要求系统模块M被称为可容许的，如果另外，它的每个重写规则t→ tJ，如果C1≥... C n满足第2.1节中的受理要求（i）-（iii）以及附加要求(iv) 如果Ci是重写ui→uJi，则vars（ui）vars（t）vars（t）i−1j=1vars（Cj），而uJi是（M）-模式，因为（M）是作为模M的基础的方程理论。在操作上，我们试图通过将实例σ（ui）关于方程约化为标准形式vi来满足这样的重写条件，然后试图找到一个重写证明vi→wi，其中wi是关于并且使得wi是uJi的替换实例。对于功能模块，当在允许的系统模块中执行条件规则时，从左到右依次尝试满足其所有条件;但请注意，现在，除了由于等式公理的存在而可能存在许多等式条件的匹配之外，我们还必须处理解决重写条件需要搜索的事实，包括当先前的解决方案不能满足后续条件时搜索新的解决方案。因此，默认解释器将支持搜索计算，并允许通过适当的参数控制搜索。一般来说，由默认解译器求解的目标可以是重写、成员资格和等式的合取，并对合取中新变量的出现进行适当的限制我们通过[16]中的一个可接受的模块来说明系统模块的新语法，[20]以这种方式转换对应于重写。 完整的CCS被表示，包括（可能是递归的）通过上下文的过程定义。读者可以在附录A.2中找到定义语法的模块。modCCS-SEMANTICS-TRANS正在保护CCS-CONTEXT。对ActProcess进行排序。subsort进程 ActProcess。* {A}P表示进程P执行了A varsL M：Label操作。var A：Act.vars P P ' Q Q'：过程。var X ：ProcessId。* 前缀rl [n]：A. P => {A}P。* 求和crl[sum]：P +Q=>{A} P' i如果P => {A}P'。C LAVELet al.8一个k1−→···−→* 组成crl [par]：P |Q => {A}（P '|Q） 如果P => {A}P'。crl[par]：P |Q=>{tau}（P '|Q '）如果P =>{L}P' /| Q => {~ L} Q '。* 限制crl [res]：P\L => {A}（P/\（A =/= L）=true/\（A =/=~ L）=true。* 重新标记如果P => {L}P'，则crl [rel]：P[M/L]=> {M}（P ' [ M / L ] ） 。crl [rel]：P[M/L]=>{~ M}（P ' [ M / L ] ） ， 如 果 P = > { ~ L }P'。crl [rel]：P[M/L] => {A}（/\（A =/= L）=true/\（A =/=~ L）=true。*** 定义crlX => {A}P/\def（X，context）=> {A}P恩德姆Maude中CCS的这种表示在语义上是正确的，因为给定CCS进程P，存在进程P1，.，P k−1，使得P−a→1 Pa2ak−1P−→PJ当且仅当P可以重写为{a1}. {ak}P（见[16]）。2.3面向对象模块许多Maude应用程序基本上使用了面向对象的模块（例如，参见调查论文[8，19]），即指定分布式对象系统的模块，其中分布式状态的顶层结构是对象和消息的关联和可交换的多集。面向对象模块的默认执行是使用此类模块进行规范和编程的最常见方式。也就是说，尽管使用适当的策略来形式化地分析面向对象的规范是非常有用的，但是很好地支持它们的默认执行也是非常重要的问题是，由先前的缺省解释器支持的公平性的一般概念这是因为，由于每个对象都有一个单独的身份，公平性现在应该局限于单独的对象和消息，即使其他类似的对象和消息被重写，也不应该被饿死。因此，Maude 2.0默认解释器将支持一种特殊的策略来执行面向对象的模块，以确保对象和消息的公平性。这种公平执行策略的直观想法可以通过一个比喻来解释，在这个比喻中，我们把对象和消息看作是像汽车一样需要汽油才能运行的实体。然后，默认策略会不时地用gas重新填充这些实体，任何重写都会减少gas的数量，但在没有更多进展之前，不允许进行新的重新填充这样，所有k−1C LAVELet al.9配置中的对象和消息被反复给予重写的公平机会这种对象的默认策略还有一个重要的额外优点，即使用内置对象，如Internet套接字、文件系统或窗口系统（见3.2节），可以很容易地以真正一致和公平的方式执行由普通对象和内置对象组成的面向对象配置2.4参数化模块与理论Full Maude 1.0模块代数支持Clear/OBJ风格的非常强大的模块组合操作。这些操作使用涉及三个关键实体的范畴结构：• 模块，这是一个初始的理论，或者在参数化的情况下，自由扩展语义;• 理论，具有松散的语义，可用于指定模块的参数并声明正式断言;• 视图，是用于实例化参数理论、细化规范和断言形式属性的理论解释。很久以前人们就知道，基于这些原语的模块代数的全部通用性和功能需要参数化的理论和视图，而不仅仅是参数化的模块。然而，目前OBJ3、CafeOBJ和Maude 1.0都不支持参数化的理论和观点。这种情况将在Maude 2.0中通过Full Maude 2.0模块代数得到补救，其中模块，理论和视图都可以参数化。通过使用参数化的理论和视图，我们可以以一种更渐进的方式实例化参数化的理论和模块，从而获得灵活性并能够精确地指定预期的应用。使用参数 化视 图将 允许 我们 ，例如，定义视图 Set[X：： TRIV]从TRIV 到SET[X：： TRIV]，将排序Elt映射到排序Set[X]。对于这种视图，我们将目标模块的参数部分保持为参数。例如，给定从TRIV到NAT的视图Nat，我们可 以 有 自 然 数 集 合 列 表 的模 块 LIST[Set[Nat]] ， 或者 给 定堆 栈 的模 块STACK[X ： ：TRIV] 和 从 TRIV 到 内 置 模 块 BOOL 的 视 图 Bool 的STACK[Set[Bool]]。有关更多详细信息，我们请读者参阅配套文件[10]，其中解释了FullMaude 2.0的关键设计概念和构造，并通过示例进行了说明。3内置模块Maude包括一些内置模块，在Maude系统内提供方便的高性能功能，以及与其他设备的有效连接。C LAVELet al.10利益系统。特别是，Maude 2.0将提供内置的机器整数，自然数和浮点数，引用标识符，字符串和互联网套接字。我们还在为有理数、文件系统和窗口系统设计潜在的内置模块。3.1功能内置模块函数内置的机器整数、自然数和浮点数、引用标识符和字符串模块为Maude程序员提供了一组最小的高效实现结构。机器整数允许Maude程序员处理机器特定的最小和最大数之间的固定长度的二元表示。对机器整数的操作采用对这些二进制表示的常数时间在Maude中，通过使用这种内置模块，可以实现对机器整数进行简单算术运算的C类性能。内置的自然数弥补了具有显式后继函数的干净的Peano类公理化与无界自然数算术的更有效的二进制表示这个内置模块将允许程序员操作数字，就好像它们是用显式的后继符号表示的一样，并将这些数字反映到元级别（和元-元级别等）。浮点数模块允许Maude用户在底层硬件平台支持时访问IEEE-754双精度浮点运算引用标识符允许Maude用户创建新名称，并以有效的方式操作包含符号的内置字符串是最近的工作领域。内置字符串，特别是8位字符的标准字符串，对于实现Internet编程、文件处理和某些输入输出过程所需的性能和表现力至关重要。在当前的版本中，Maude将来，可能需要将此覆盖范围扩展到其他字符集约定，如Unicode。Maude一个字符串标识符是一个Maude标识符，它只包含一对匹配的“s”，这是它的第一个和最后一个字符。当字符串标识符被解析为字符串时，它会使用ANSI C反斜杠转义约定的子集进行解释[13，Section A2.5.2]。长度为1的字符串形成子排序字符串。内置字符串的当前实现包括在附录B中简要描述的函数Maude字符串包与QID内置模块[5]兼容，并与Maude 2.0方案互操作，用于元表示用户常量。C LAVELet al.113.2面向对象的内置模块面向对象观点的一个重要优点是，外部世界中的所有类型的实体都可以被概念化为对象，并且可以通过消息传递从计算中进行交互在Maude之前的版本中，除了LOOP-MODE模块支持的文本交互外，所有与对象的交互都可以在Maude中指定和模拟在Maude 2.0中，内置对象通过接口扩展了Maude，允许与外部实体（如Internet套接字、文件系统、窗口系统等）进行交互。通过这种方式，计算可以与外部世界以及不同机器中的其他Maude计算以分布式方式连接。到外部实体的接口可以在定义内置对象的内置面向对象模块这种内置的面向对象模块可以由普通的面向对象模块导入，因此，一般来说，计算的面向对象状态由两部分组成：• 普通对象和消息的配置，在Maude中表示为表示这些对象和消息的多项集合，以及• 一组内置对象，以及与这些对象往来的消息从概念上讲，我们可以把这两部分看作是对象和消息的一个更大的配置然而，内置对象本身在普通对象和消息的配置中不可见，除非通过它们发送的消息间接可见。特别是，内置对象的内部结构是隐藏的，因此它们只能通过异步消息传递进行交互。包含内置对象的部分还包含一个系统对象或原型对象[18，4.4节]，它负责回答创建新内置对象的请求，并将新对象的名称发送给请求对象，以及回答类特定的查询一般来说，普通对象和消息的配置与内置对象之间的消息双向传输包括：(i) 创建内置对象的请求，以及向请求者提供新名称的应答，(ii) 对系统对象的类特定查询，以及相应的答案，以及(iii) 从普通对象到内置对象的消息，并在另一个方向上回复消息我们在下面用目前正在实现的内置互联网套接字类来说明这些想法2系统类由所有内置类导入，但它可以通过子类化以提供特定于类的查询的答案。C LAVELet al.123.3内置互联网插座也许面向对象的内置模块中最有趣的是互联网套接字接口，旨在支持互联网编程。因特网计算对程序员和语言实现者提出了与传统顺序计算不同的问题。特别是，由于典型的处理速度和典型的互联网连接之间存在千倍的差异，因此诸如对资源的非阻塞访问和公平性的原生概念等问题比原始速度或其他语言选择考虑要重要得多。Maude非常适合支持互联网编程。Maude中原生的、语义上干净的并发方法提供了一个干净的基础。 重写逻辑规范和任何兼容实现的固有公平非阻塞特性为互联网环境中顺序语言中笨拙的线程实现提供了一种受欢迎的替代方案。实际上，Maude的 设 计 本 质 上 提 供 了 网 络 通 信 的 多 路 复 用 。互联网编程是通过一套统称为TCP/IP的协议来完成的这些协议包括IP，原始互联网协议（运行在硬件协议之上），以及两个构建在IP之上的协议，UDP，用户数据报协议和TCP，传输控制协议。在网络堆栈的更高级别依次构建的更高级别协议包括DNS，域名系统（UDP之上），HTTP，超文本传输协议，FTP，文件传输协议和SMTP，简单邮件传输协议（所有三个都在TCP之上我们设计了一个简化的Maude API到DNS和TCP，这样其他建立在TCP之上的应用程序协议可以在Maude中有效地实现。这个包大量使用了内置字符串，这已经在3.1节中描述过了在实现内置sock-ets的背后有三个基本思想。首先，我们包括一个系统对象，它可以发送消息，可以创建其他特殊对象并返回句柄（对象标识符）。第二，大多数系统调用（或系统调用序列）将被包装为一对消息，一个用于启动调用（或序列），另一个用于返回结果。对于许多操作，这提供了必要的序列化，并且是来自顺序语言（如C）的系统调用所固有的第三，TCP/IP有多种API，但AF INET套接字几乎在每个平台上都可用。因此，我们提供了套接字级接口作为Maude中Internet编程的基本公共机制附录C包括一个用户如何使用内置Maude套接字接口构建一个非常简单的HTTP/1.0客户端的示例，用于从Internet上的任意位置检索网页。我们相信，Maude内置了对套接字的支持，将为互联网编程提供一个强大的C LAVELet al.13当前一代的解释型多线程语言，如Java [12]和Python [24]。我们目前正在研究Maude专用传输协议的优点，该协议建立在TCP之上，称为移动对象传输协议（MOTP），将用于Mobile Maude，Maude 2.0的移动语言扩展[9]。4新的META-LEVEL除了允许扩展模块语法和新内置模块的元表示外，新META-LEVEL的两个关键新优点是：更简单的术语表示和更丰富的下降函数集[4]。4.1排序和种类表示排序和种类被表示为引用标识符的排序Qid的特定子排序。 由于运算符声明可以同时使用排序和种类，我们用Type表示排序和种类的并集。subsorts排序种类类型Qid.子排序类型<类型列表。4.2Term表示项的更简单的表示是通过Qid的子排序Constant和Variable获得的。常量是带引号的标识符，它包含常量的名称和类型，由“分隔。“，例如，’0.Nat类似地，变量包含由“：“分隔的名称和类型，’N:Natappropriate选择器然后提取它们的名称和类型.子排序常量变量QID。op getName：Variable -> Qid.op getType：Constant -> Type。操作getType：Variable->Type。然后用通常的方法构造一个项，通过将一个运算符符号应用于一个项列表，常量和变量是构造中的基本情况。子排序常量变量<项。op_[_]：Qid TermList -> Term. 子排序术语<列表。op _，_：TermList TermList -> TermList [asclock].通过这种方式，常量和变量由原子实体元表示即由特殊类型的引用标识符元表示;任何更高级别的元表示都不会增加它们的大小：它只是增加了一个引用。例如，模块NAT中的项s（N：Nat）+0现在元表示为'_+_['s 'N：Nat]，'0.Nat]并由'_'[_']''_+_，'_'，_'_'[_']''s，''N：Nat]，'' 0.Nat]]C LAVELet al.14有两种特殊的操作来构造（布尔）术语，对应于成员关系测试和成员关系惰性测试：op_：：_：术语排序->术语。op_：_：术语排序->术语。4.3模块表示模块本质上是元表示的，如[4]中所解释的，但有以下不同之处：我们需要条件成员关系，等式和规则中的新条件的语法;不需要变量声明;术语现在使用术语的新元表示。操作fmod_is_sorts_。endfm：QidImportListSortSetSubsortDeclSetOpDeclSetMaxAxSetEquationSet ->FModule。操作mod_is_sorts_。 endm：QidImportListSortSetSubsortDeclSetOpDeclSetQid AxSetEquationSet RuleSet ->Module.subsort排序_[_].） ：Qid TypeList Type AttrSet-> OpDecl.op _=_ ： Term -> EqCondition [ctor]. op_ ： _ ： Term Sort -> EqCondition [ctor].op _ ： =_：Term Term -> EqCondition[ctor].op_/\_：EqCondition EqCondition -> EqCondition[ctorasparity]. 子排序EqCondition<条件。op _=>_：Term Term -> Condition [ctor].op _/\_：Condition Condition -> Condition [ctor assistance].操作mb_：_。：术语排序-> Ax [ctor]。操作cmb_：_if_。：Term Sort EqCondition ->Ax[ctor]。操作等式_=_。： Term Term-> Equation[ctor]。操作ceq_=_if_。：Term Term EqCondition ->Equation[ctor]。操作rl[_]：_=>_。：Qid Term Term->Rule[ctor].操作crl[_]_=>_if_. ：Qid Term Term Condition -> Rule [ctor].举一个非常简单的例子，左边模块的元表示是右边显示的术语，这样读者就可以理解两种符号之间的相似性：fmod NAT是fmod无排序Zero Nat。sort 'Zero ; 'Nat.subsort ZeroZero [ctor].op' 0 ： n i l- >' Z e r o[ c t o r ] .ops：Nat -> Nat [ctor].op' s ： ' N a t - > ' N a t [ c t o r ] .op _+_：Nat Nat -> Nat [].op'_+_：'Nat 'Nat -> 'Nat []. varsNM：Nat.没有一等式0 + N = N。等式“_+_n”0.Nat，“N：Nat]=”N：Nat.C LAVELet al.15eqs（N）+M=s（N+M）。eq '_+_['s 'N：Nat]，'M：Nat]=’s[’_+_[’N:Nat, ’M:Nat]]endfm endfmC LAVELet al.164.4下降函数我们已经向前面的下降函数MetaApply、MetaReduce和MetaRewrite添加了一个新函数MetaMatch，以便实现将模式与顶部的主题词匹配的元级等效，以及通用化函数MetaXapply和MetaXmatch，它们分别应用规则或尝试不仅在主题词的顶部，而且在其中的任何地方进行匹配，并且进一步扩展。函数metaApply直观地将给定模块（第一个参数）中的规则（其标签是第由于运算符的结构公理可能有几个可能的匹配，最后一个结果是一个术语，带有相应的排序或种类，以及匹配的替换。函数metaXapply做同样的事情，但是使用扩展（参见[6，Section- tion5.8]）并且在任何可能的位置，而不仅仅是在顶部。最后一个参数指出了规则可以应用于的被关注项的深度（相对于其结合或结合交换算子）。结果有一个额外的组成部分，给出了重写发生的给定项内的上下文op metaApply： Module Term QidSubstitution MachineInt-> [ResultTriple].操作meta Xapply：Module TermQid Substitution MachineInt MachineInt->[Result4Tuple].op {_，_，_}：Term Type Substitution -> ResultTriple [ctor].op {_，_}：Term Type Substitution Context -> Result4Tuple [ctor].函数metaMatch直观地尝试匹配模块中的前两个最后一个参数用于枚举可能的匹配。如果匹配尝试成功，则结果是相应的替换。metaXmatch的推广遵循与以前完全相同的思想。opmetaMatch：Module Term Term MachineInt->[Substitution].opmetaXmatch：Module Term Term MachineInt MachineInt->[MatchPair]. op {_，_}：Substitution Context -> MatchPair [ctor].下降函数MetaReduce和MetaRewrite与以前的版本相比没有变化，但它们的结果现在包括了结果项的排序或种类操作MetaReduce：Module Term-> [ResultPair]。op metaRewrite：Module Term MachineInt -> [ResultPair].op{_，_}：Term Type-> ResultPair [ctor].我们还在考虑添加用于统一的函数metaUnify，MetaSearch用于内置搜索。C LAVELet al.17/5其他功能5.1Maude模块系统Core Maude中的Maude模块系统已经完全重写，以支持延迟重解析和延迟重解析，并且已经在Maude 1.0.5中可用。惰性重定向意味着当用户进入一个结构化很强的Maude模块时，签名会像往常一样被重定向，但成员资格、等式和规则只会在输入重写命令这节省了大量的内存并加快了模块的输入速度，但是：（a）成员关系、方程和规则中的某些错误可能要到重命名发生时才能被捕获;（b）在模块中第一次执行重写命令之前有一个短暂的停顿，而重命名已经完成;（c）不同模块中出现的方程和规则的顺序已经改变。模块自己的方程和规则现在位于导入的方程和规则当然，用户不应该依赖于此。惰性重解析意味着当输入一个与现有模块同名的模块时，它会替换旧模块，并且依赖于旧模块的所有模块都被标记为过时，并且如果试图使用它们，则会重新解析旧模块5.2LATEXPRETTY印刷Maude2.0支持直接打印到LATEX。 可以通过命令set print latex on打开或关闭LATE X日志记录。把指纹乳胶擦掉默认情况下，关键字设置为粗体，术语在数学模型中使用各种各样的概念进行键入，以便从其多字符ASCII版本，例如：x2变为x2，>=变为≥，===.一个TLEX宏可以针对每个具有以下功能的操作器进行专门设计latex属性，例如：opdefiniteIntegral： Exp Exp Exp Var-> Exp[latex（{\int_{#1}^{#2}{#3} d{#4}}）]。词法分析是使用分隔符中的LATEX连接来完成的;结果扩展的字符串然后由yLATEXnewcommand定义。在这种情况下，Maude2.0支持自动打印到LATEX。6Maude餐厅Maude编译器处于原型开发阶段，但已经能够支持Maude解释器所接受的语言的大子集。随着编译技术的发展，编译器的覆盖范围将不断扩大。Maude编译器是通过将Maude 2.0程序编译为C++来实现的，每个Maude函数都有一个C++函数，然后对其进行编译C LAVELet al.18使用GNU g++来获取本地可执行文件。在某些示例中，当前的编译器可以在667MHz Xeon上达到每秒1500万次重写，比解释器在相同硬件上达到的每秒298万次重写加速了5倍在编译器中，已经进行了许多优化，这些优化显著提高了性能，包括：• 排序计算和测试是基于排序结构优化的;对于多个排序的模块，成本几乎为零。• 外自由函数符号骨架采用多对一判别网。我们采用了这一点很重要，因为当前的GNU g++不能够分割活动变量范围，而这在类似Intel x86的架构上很• 表示术语图的节点具有可变大小（与解释器中的固定大小dag节点相比），因为我们不需要能够用另一个dag节点覆盖一个dag节点（就地替换），并且我们不必担心碎片化，