Maude中的数据结构及其规范和证明方法

理论计算机科学电子笔记137（2005）105-132www.elsevier.com/locate/entcsMaude中的数据结构Narciso Mart 's-Oliet，Miguel Palomino，and AlbertoVerdejoDepartamentodeSistemasInforicosyProgramacionUniversidad Complutense de Madrid{narciso，miguelpt，alberto}@ sip.ucm.es摘要本教程描述了Maude中一系列典型数据结构的等式规范。我们从众所周知的栈、队列和列表开始，继续二叉树和搜索树。不仅考虑了简单的版本，而且考虑了高级版本，如AVL和2-3-4树。 Maude中可用的运算符属性允许基于满足某些等式属性的构造函数来指定数据，例如关联列表的串联，并将空列表作为标识，而不是其他函数式编程语言中可用的自由构造函数。 此外，Maude所基于的等式逻辑的表达版本，即成员等式逻辑，允许忠实地指定类型，其数据不仅通过构造器来定义，而且还通过满足其他属性，如排序列表或搜索树。 在本文的第二部分中，我们描述了一个归纳定理证明，ITP，这本身是开发和集成在Maude的强大的metallevel和metalanguage功能，由后者提供，以证明数据结构的属性。这是正在进行的工作，因为ITP仍在开发中，一旦数据变得有点复杂，其属性的证明就会变得更加复杂。关键词：数据结构，代数规范，隶属方程逻辑，莫德，归纳定理证明。1介绍Maude是一种基于重写逻辑的声明式语言和系统[6，5]。尽管语言和系统都在不断改进，*研究部分得到MCyT西班牙项目MIDAS（TIC 2003MELODIAS（TIC 2002 -01167）。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.01.041106N. Martí-Oliet等人/理论计算机科学电子笔记137（2005）105随着2003年夏天第2版的公开发布，它已经成熟。从那时起，Maude在世界各地的教学和研究中被使用，特别适用于逻辑系统、编程语言和一般计算系统的规范和原型设计。然而，仍然缺乏可以共享和重用的公共库。本教程试图通过提供Maude中指定的典型数据结构库来填补这一空白。这是通过更新和大大扩展Maude [4]第1版发布的教程中提供的规范集来实现的。更具体地说，我们首先描述基本数据类型的众所周知的版本，如堆栈，队列和列表;然后我们继续几个版本的树，包括二叉树，一般树和搜索树;我们不仅考虑简单的版本，而且还考虑高级版本，如AVL，2-3-4和红黑树;最后，我们描述了优先级队列的抽象版本和基于左树的更具体的版本。对于所有这些规范，我们不需要考虑重写逻辑的全部一般性，而只需要考虑它的等式子逻辑，即隶属等式逻辑[11]（从Maude语言的角度来看，我们所有的规范都是函数模块）。非常重要的一点是，这种等式逻辑的表达性允许忠实地指定类型，这些类型的数据不仅通过构造器来定义，而且还通过满足附加属性来定义，如排序列表，搜索树，平衡树等。我们将在本文中看到这是如何通过成员关系断言来实现的，这些断言等式地描述了相应数据所满足的属性。我们考虑的所有数据类型都是通用的，也就是说，它们是在构造中作为参数出现的其他数据类型之上的因此，我们的规范是参数化的，因此，我们使用Full Maude [6]，它提供了强大的参数化机制，该机制基于描述数据类型必须满足的构造才有意义的理论例如，列表可以在任何数据之上构造，但排序列表只对具有全序的数据有意义;对于一个全序的二元运算，必须满足几个性质，这些性质在相应的参数理论中被写成方程。我们假设一些关于指定的数据结构的知识。有许多教科书描述了众所周知的命令式和面向对象的实现[9，2，16]。不太为人所知，但对我们的目的非常有用的是函数式编程语言（如ML）N. Martí-Oliet等人/理论计算机科学电子笔记137（2005）105107或Haskell [12，15，14];在某些情况下，我们的方程与这些文本中给出的方程非常相似另一方面，我们并不假设有太多关于Maude的知识，因此我们描述了主要特征，因为它们与规格一起出现。如前所述，这里我们根本不考虑Maude中基于规则的编程。有关这些功能的介绍，我们请感兴趣的读者参阅论文[13]。本文中的所有代码和更多内容可以在网页中找到[10]。2审查主要特点2.1功能模块Maude中的函数模对应于代数方程逻辑中的方程理论。逻辑和语言都是类型化的，类型通过关键字sort或sort声明。然后，通过关键字op引入的每个运算符都必须与其参数的排序和结果的排序一起声明。类型之间存在包含关系，这通过子排序声明来描述。运算符可以重载。有了类型化变量（可以单独声明，也可以在- the-numbery上使用相应的排序）和运算符，我们可以用通常的方式构建术语。一个给定的术语可以有许多不同的排序，因为子排序和重载。在一些容易满足的要求下，一个术语有一个最小的排序。术语用于形成• 成员关系断言t：s（由关键字mb引入），声明术语t具有排序s，以及• 等式t=tJ（用关键字eq引入），说明项t和tJ的含义相同。成员资格和方程都可以是有条件的，分别使用关键字cmb和ceq。条件由方程和成员的结合（写作/\）形成函数模块中的计算是通过使用方程作为从左到右的简化规则来进行的，直到达到规范形式。为了使这一点有意义，方程右边的变量必须包含在左边的变量中（我们将在后面看到，通过在条件中匹配方程来提供推广）;此外，方程组必须是终止的和连续的。这保证了所有的项都将简化为唯一的标准形式[1]。108N. Martí-Oliet等人/理论计算机科学电子笔记137（2005）105有些方程，如交换性，不是终止的，但它们仍然通过算子属性来支持，因此Maude对这些属性提供的方程理论进行模简化，这些属性可以是结合性，交换性，恒等式和恒等式。像终止和连续这样的性质应该在模简化某些方程理论的更一般的背景下理解模块可以以不同的模式导入。最重要的一个是保护，它断言导入模块中的所有信息不会因为导入而改变;更具体地说，导入模块中的不同数据不会在导入模块中被识别，并且没有新数据添加到导入的排序中。如果不是这种情况，输入模式可以是包括。2.2参数化正如我们已经提到的，参数化数据类型使用理论来规范参数必须满足的要求。一个（泛函）理论也是一个隶属方程的规范，但由于它的方程不用于方程的简化，它们不需要满足任何关于变量在右边、连续性或终止性的要求。最简单的理论是只需要存在一个类的理论，如下所示：(fth TRIV是一种Elt。endoscopy）该理论被用作参数化数据类型（如堆栈、队列、列表、多集、集合和二叉树）的参数要求下面是一个更复杂的理论，要求给定排序的元素有（严格）全序注意第一个条件方程右边的新变量E2。这使得该公式不可执行，如公式旁边的属性nonexec(fth TOSET<正在保护BOOL。分类Elt.操作_<>_：Elt Elt-> Bool。vars E1 E2 E3：Elt.等式E1 E2 = E2 Stack（X）[ctor].oppush：X@Elt Stack（X）-> NeStack（X）[ctor]. oppop：NeStack（X）-> Stack（X）.top：NeStack（X）-> X@Elt.opisEmpty：Stack（X）->Bool.var S：Stack（X）.var E：X@Elt. 等式pop（push（E，S））= S。等式top（push（E，S））= E。eq isEmpty（empty）= true。eq isEmpty（push（E，S））= false。endfm）下面的视图将理论TRIV映射到整数的预定义模块INT，然后在一个项归约的例子中使用，用Maude命令red调用。(view 从TRIV到INT的Int排序为Elt到Int。endv）Maude>（STACK（Int）中的红色：top（push（4，push（5，empty）。结果NzNat：4请注意，Maude计算结果的最小排序3.2队列队列的规范与堆栈的规范非常相似，因此这里不包括它。它在[10]中可用。N. Martí-Oliet等人/理论计算机科学电子笔记137（2005）1051113.3列出我们将以两种方式指定列表，在每种情况下使用不同的构造函数集在这两种情况下，列表都是相对于TRIV理论参数化的。第一个版本使用了两个在许多函数式编程语言中都可以找到的标准自由构造函数：空列表nil，这里用常量[]表示，以及cons操作，它将一个元素添加到列表的开头，这里用mix fix语法_：_表示。通常，head和tail是与这个构造函数关联的选择器。由于它们没有在空列表上定义，我们通过非空列表的子排序NeList来避免它们的重复，就像我们对栈所做的那样（见3.1节）。列表上的其余操作（通常由两个构造函数上的结构归纳定义）连接两个列表，计算列表的长度，并反转列表;其中第二个操作的排序结果Nat来自导入的（在保护模式下）预定义模块NAT。由于解析限制，在Full Maude中声明某些字符（[ ]{ }，）时，必须在其前面加上反引号(fmod LIST（X：：TRIV）正在保护NAT。sortNeList（X）List（X）.（X）<函数的值为0。op'']：->List（X）[ctor].OP _：_：X@Elt List（X）-> NeList（X）[ctor]. 操作tail：NeList（X）->List（X）。ophead：NeList（X）-> X@Elt.op _++_：List（X）List（X）->List（X）. 操作长度：List（X）-> Nat.操作rev：List（X）-> List（X）。var E：X@Elt.var N：Nat.var L L '：List（X）.eqtail（E：L）= L。eq压头（E：L）=E。eq[]++ L = L。等式（E：L）++ L ' = E：（L ++ L'）。eq length（[]）= 0。等式长度（E：L）= 1 +长度（L）。eq rev（[]）=[]。eq rev（E：L）= rev（L）++（E：[]）。endfm）让我们考虑一个约简的例子，看看我们认为是未定义的项会发生什么：空列表的头部。Maude>（LIST（Int）中的红色：head（[]）。）result [Int]：head（[]）请注意，Maude返回了未约化的项，并赋予它一种（[Int]）而不是排序。人们可以把一种错误看作112N. Martí-Oliet等人/理论计算机科学电子笔记137（2005）105其中，除了正确的格式良好的术语之外，还有未定义的或错误的术语。在Maude中，类型没有显式声明，并且用相应的排序周围的方括号表示。Maude在解析时也使用类型，如下例所示。Maude>（LIST（Int）中的红色：头（尾（1：2：[]））。）结果NzNat： 2正如预期的那样，上面约简的结果是列表2：[]的第一个元素（2），它是从最初的一个元素中去掉头部得到的然而，注意根据tail操作符的声明，tail（1：2：[]）项的最小排序是List（Int），而head操作符需要一个非空列表作为参数。 一旦tail（1：2：[]）项使用最小排序NeList（Int）减少为2：[]，这种差异就会消失。在解析时，这个信息还不知道，但Maude通过隐式地假设运算符声明在类的级别上并在这个级别上解析它们，给了这些术语怀疑的好处。当然，像head（true）这样格式不好的术语在解析时仍然会被拒绝。1Maude>（LIST（Int）中的红色：head（true）。）错误：命令不正确。另一种生成列表的方法是从空列表和单例列表开始，然后使用连接操作来获得更长的列表。然而，连接不能是自由列表构造函数，因为它满足结合方程。这个等式不是直接声明的，而是作为一个运算符属性声明的.此外，还存在关于空列表的串联的身份关系，其通过属性id：[]来表示。这里使用空的并置语法（在下面的模块中声明）将连接运算符作为构造函数是非常方便的;这样，前面的表示法中的整数列表1： 2： 3：[]现在就变成了简单的1 2 3。注意单例列表是如何用相应的元素来标识的（通过子排序声明X@Elt NeList（X）），以及连接运算符是如何子排序重载的，有一个声明用于非空列表，另一个声明用于列表，两者具有相同的属性。还有两种可能的串联重载（NeListList1Core Maude能够提供有关解析错误的更多信息：红色的头（真的）。警告：标准输入>，第2行：<警告：标准输入>，第2行：没有解析术语。N. Martí-Oliet等人/理论计算机科学电子笔记137（2005）105113-> NeList和List NeList -> NeList），但在这种情况下它们是不必要的，因为标识的属性。最后，注意重载操作中的运算符属性必须一致，尽管，通过单独阅读第二个连接声明，说空列表是仅在非空列表上定义的操作的标识听起来有点奇怪。当一个operator有许多重载声明时，可以使用operator属性ditto来隐式重复属性，而不必再次显式写入所有属性由于算子的属性，在其上进行简化的同余类是模结合性和恒等式计算的。因此，我们只需要两个方程来完全指定定义的操作的行为，如长度和转速;单例情况包括在E L的情况下，通过实例化变量L与常数nil和应用属性的身份。注意，这样，即使我们改变了列表构造函数的集合，我们并没有通过对其余操作的结构归纳来改变定义的风格（除了符号）;情况E L对应于前面规范中的cons情况。(fmod LIST-CONCAT（X：： TRIV）是保护NAT。sort NeList（X）List（X）.（List（X）[ctor].op ：List（X）List（X）-> List（X）[ctor asynchronid：'']]。op：NeList（X）NeList（X）-> NeList（X）[ctorasynchronid：'']]. 操作tail：NeList（X）-> List（X）。ophead：NeList（X）->X@Elt. 操作长度：List（X）-> Nat. 操作rev：List（X）-> List（X）。varE：X@Elt.varL：List（X）. eq tail（EL）= L。eq压头（EL） =E。eq长度（nil）= 0。等式长度（E L）= 1 +长度（L）。eq rev（nil）=nil。eq rev（E L）= rev（L）E。endfm）3.4有序列表在有序的等式规范中，子排序必须通过构造器来定义，但是不可能有有序列表的子排序，例如，通过列表上的属性来定义;需要一种更具表达性的形式主义。成员关系等式逻辑允许通过涉及等式和/或排序谓词的条件来定义子排序。在这个例子中，我们使用114N. Martí-Oliet等人/理论计算机科学电子笔记137（2005）105这种技术定义了一个子排序OrdList，包含有序列表，2列表的排序列表，这是从模块LIST中导入的3.3节。注意定义排序OrdList的三个（条件）成员公理：空列表和单例列表总是有序的，当第一个元素小于或等于第二个元素时，一个较长的列表是有序的，没有第一个元素的列表也是有序的。参数化有序列表需要比TRIV更强的要求，因为我们需要对要排序的元素进行全序。我们在2.2节中看到的TOSET理论要求元素有严格的全序;由于重复不会给列表排序带来任何麻烦，我们可以在要求中使用_=_我们也可以导入理论（在包含模式中），因此我们可以如下定义我们的理论(fth TOSET< =包含TOSET<。op_<=_：Elt Elt-> Bool.vars X Y：Elt.等式X = Y = XY或X == Y。endoscopy）有序列表的参数化模块将导入参数化列表模块。然而，请注意，我们想要的是全序集合的列表，而不是任何集合上的列表;因此，我们从理论TRIV到理论TOSET =(view Toset from TRIV to TOSET< =是从Elt到Elt排序。endv）我们仍然剩下一个参数化的模块和相应的依赖排序，但是现在是关于TOSET = 需 求 。 这 就 是 为 什 么 在 下 面 的 保 护 性 导 入 中 使 用 符 号 LIST（Toset）（X），以及在导入的排序名称中使用NeList（Toset）（X）和List（Toset）（X）作为这个有序列表模块的一部分，我们还定义了几个著名的排序操作：插入排序，快速排序和合并排序（以下代码只包括第一个，而其他两个可以在[ 10 ]中找到更完整的版本）。它们中的每一个都使用了适当的辅助操作，其行为是预期的;例如，insertion-sort递归地对没有第一个元素的列表进行排序，然后调用insert-list，将缺失的元素插入正确的位置。重要的一点是，我们能够为所有这些排序操作提供比其他代数规范框架中的通常类型更好的类型。2.我们更喜欢N. Martí-Oliet等人/理论计算机科学电子笔记137（2005）105115函数式编程语言。因此，插入排序被定义为从List（Toset ）（X）到OrdList（X）的操作，而不是从List（Toset）（X）到List（Toset）（X）的信息量少得多的类型。这同样适用于每个辅助操作。此外，一个要求其输入参数是有序列表的函数现在可以定义为全函数，而在表达性较低的类型形式主义中，它必须是部分的，或者在错误参数上定义异常行为。(fmod ORD-LIST（X：： TOSET =）是保护LIST（Toset）（X）。sorts（X）NeOrderList（X）.Subsort NeOrderList（X）OrderList（X）NeList（Toset）（X） OrdList（X）.opinsert-list：OrdList（X）X@Elt -> OrdList（X）.vars N M：X@Elt.var L L '：List（Toset）（X）. vars OL OL '：OrdList（X）.var NEOL：NeOrderList（X）.mb []：OrderList（X）.mb（N：[]）：NeOrderList（X）.cmb（N：NEOL）：NeOrderList（X），如果N<= head（NEOL）。eq insertion-sort（[]）=[].eqinsertion-sort（N：L）=insert-list（insertion-sort（L），N）. eqinsert-list（[]，M）= M：[].ceq插入列表（N：OL，M）=M：N：OLifM<=N。ceqinsert-list（N：OL，M）= N：insert-list（OL，M）ifM > N . endfm）3.5多重集与连接的结合性和恒等式为列表（或字符串）提供结构公理的方式相同，我们可以通过考虑一个联合构造函数（再次使用空的并置语法编写）来指定多集，该构造函数满足结合性、交换性（因为现在元素之间的顺序无关紧要）和恒等式结构公理，所有这些公理都被声明为属性。单吨多重集是用元素来标识的，就像我们对列表所做的那样，通过声明X@Elt作为Mset（X）的子排序。(fmod MULTISET（X：： TRIV）是保护NAT。sortMset（X）.（ Mset（X）[ctor].op：Mset（X）Mset（X）-> Mset（X）[ctor asynchronid：empty]. opsize：Mset（X）-> Nat.op mult：X@Elt Mset（X）-> Nat.操作删除：X@Elt Mset（X）-> Mset（X）。opis-in：X@Elt Mset（X）-> Bool。变量E E ' ： X @ E l t.var S：Mset（X）. eq size（empty）= 0.等式size（E S）= 1 +size（S）。116N. Martí-Oliet等人/理论计算机科学电子笔记137（2005）105eq mult（E，empty）= 0。等式mult（E，E S）= 1 + mult（E，S）。如果E =/= E'，则ceq mult（E，E' S）= mult（E，S）。eq delete（E，empty）= empty.eq delete（E，E S）= delete（E，S）.如果E =/= E'，则ceq delete（E，E' S）= E' delete（E，S）。eqis-in（E，S）= mul t（E，S）>0。endfm）3.6集类似于通过增加交换性从列表中获得多集，人们可以通过增加幂等性从多集中获得集合。 在当前版本中Maude的结合性和幂等性的运算符属性是不兼容的，但这很容易通过添加结合性的运算符属性和幂等性的显式方程来解决。由于集合的具体化与前面的多集合的具体化非常相似，我们参考[10]。3.7二叉树二叉树（相对于TRIV参数化）是用两个自由构造器构建的：空树，用常量empty表示，以及一个操作_[_]_，它将一个元素设置为两个给定树（它的左子树和右子树）上的根。与这个构造函数相关联的三个选择器（root、left和right）只对属于相应子排序的非空树有意义。计算二叉树深度（或高度）的操作在递归非空情况下调用自然数的max操作，以获得两个这样的数字的最大值。由于在预定义的模块NAT中没有提供此操作，因此我们导入一个模块NAT-MAX，该模块先前已将max操作添加到NAT中。最后，我们还有三个计算标准二叉树遍历的操作，其中List（X）作为值排序（这就是该模块导入LIST模块的原因）。由于它们都具有相同的等级，因此它们通过关键字ops一起声明。(fmod二叉树（X：： TRIV）是保护LIST（X）。保护NAT-MAX对NeBinTree（X）进行排序BinTree（X）。SubsortNeBinTree（X） BinTree（X）[ctor].操作_'[_']_：BinTree（X）X@Elt BinTree（X）->NeBinTree（X）[ctor]。ops left right：NeBinTree（X）->BinTree（X）.oproot：NeBinTree（X）->X@Elt. opdepth：BinTree（X）->Nat.N. Martí-Oliet等人/理论计算机科学电子笔记137（2005）105117操作前序后序：BinTree（X）-> List（X）。varE：X@Elt.vars L R：BinTree（X）.vars NEL NER：NeBinTree（X）. eq left（L [E] R）=L。eq right（L [E]R）=R。eq root（L [E] R）= E。eq深度（空）=0。eq深度（L [E] R）= 1 + max（深度（L），深度（R））。eq preorder（empty）=[].eq前序（L [E] R）= E：（前序（L）++前序（R））。eq inorder（empty）=[].等式inorder（L [E] R）= inorder（L）++（E：inorder（R））。eq postorder（empty）=[].eq postorder（L [E] R）= postorder（L）++（postorder（R）++（E：[]））。endfm）3.8一般树一般的树可以有一个可变数目的儿童为每个节点。可以通过使用行为类似于列表的森林的辅助数据类型来指定它们 树木的因为参数化和规范化技术与我们之前已经描述的技术没有区别，所以我们在这里不包括规范，而是再次参考[10]。3.9二叉搜索树这个例子在原理上类似于有序列表，但更复杂。我们通过在3.7节定义的二叉树的排序BinTree的项上使用几个（一致）成员公理来指定（二叉）搜索树的子排序。虽然我们允许在有序列表中重复元素，但在搜索树中不应该这样，因为所有节点必须包含不同的值。二叉查找树是一个空的二叉树或一个非空的二叉树，使得左子树中的所有元素都小于根树中的元素，右子树中的所有元素都大于根树中的元素，并且左子树和右子树都是二叉查找树。这是通过计算非空搜索树中的最小和最大元素的辅助操作来检查的，并且在删除元素时也很有用。同样，最重要的一点是，成员关系等式逻辑允许我们通过成员关系断言来定义相应的子排序（我们在下面的规范中考虑了五种情况），并以最好的方式将类型分配给为该数据类型定义的所有操作。虽然我们可以仅根据理论TOSET<给出的总顺序来参数化二叉搜索树，但我们在这里指定搜索树的版本，该搜索树包含由键及其相关内容形成的节点对118N. Martí-Oliet等人/理论计算机科学电子笔记137（2005）105所以我们把搜索树看作字典。搜索树的结构是关于一个严格的总顺序的关键字，但内容可以在任意排序。当我们插入一个对K，C，并且密钥K已经出现在树中的一个对K，CJ中时，插入通过组合内容CJ和C来进行。这种组合可以是用第二个替换第一个，只是忘记第二个，如果树用于实现多集并且Cs表示多重性，则添加等等。请注意，规范所依赖的两个参数理论是如何分开的，|.原则上，一个pair构造应该足以将我们刚刚描述的信息放在一起，但是我们将在更复杂的数据结构中导入搜索树的模块，这些数据结构恰好是搜索树的特殊情况，例如AVL和红黑树。在这些情况下，重要的是在节点中添加新信息：对于AVL树，需要在每个节点中悬挂的树的深度，而对于红黑树，需要适当的节点颜色。因此，考虑到这一点，定义一个可扩展的数据类型是很重要的，我们已经考虑了在模块RECORD中定义的记录。记录被定义为由字段名和相关值组成的对的集合（具有由_，_在导入使用Record视图实例化的二叉树之后，我们定义了键（语法键：_）和内容（语法内容：_）的字段，以及从记录中提取适当值的相应投影操作。请注意，这些操作以及树上的操作如何应用于具有更多字段的记录，此时还未知，通过使用变量Rec来处理这种向记录添加字段的构造是修改排序记录中的数据，这些数据是树的节点中的数据，因此也是树本身。出于这个原因，我们在包含模式下导入了模块BIN-TREE（在用视图Record实例化它之后）除了插入和删除操作之外，我们还有一个查找操作，当键出现在树中时，该操作返回与给定键相关的内容。然而，最后一个操作是部分的，因为当关键字没有出现在树中时，它没有定义;这种错误状态不能通过子排序来处理，因为错误条件取决于参数的具体值。我们使用了一个部分运算符声明，声明查找运算符的结果是与排序Y@Contents相关联的[Y@Contents]类型（注意排序名称周围的方括号表示相应的类型）。而不是在种类的层面上N. Martí-Oliet等人/理论计算机科学电子笔记137（2005）105119只 是 一 个 不 减 少 的 术 语 ， 我 们 已 经 声 明 了 一 个 特 殊 的 值 ， 类 型 为[Y@Contents]，当键没有出现在树中时，查找这些操作通常通过结构归纳法来指定，在非空的情况下，通过将给定的密钥K与树根中的密钥进行比较，并根据K是小于、等于还是大于根密钥来区分这三种情况。(fth 内容是排序的内容。opcombine：Contents Contents -> Contents [目录].endoscopy）（fmod RECORD是对记录进行排序。opnull：-> Record [ctor].op_'，_：Record Record -> Record [ctor aspheroidid：null].endfm）（从TRIV到RECORD查看记录是将Elt排序为记录。endv）(fmod搜索树（X：：TOSET<|Y：：CONTENTS）是BIN-TREE（记录）对SearchTree（X）排序|Y）NeSearchTree（X|Y）。子排序NeSearchTree（X| Y）<搜索树（X| Y）。子排序SearchTree（X| Y） Record [ctor]。opcontents：_：Y@Contents-> Record [ctor].未找到操作：-> [Y@Contents]。操作键：记录-> X@Elt。op contents：Record -> Y@Contents.var Rec：记录。var K：X@Elt.var C：Y@Contents.eq key（Rec，key：K）= K。eq含量（Rec，含量：C）= C。二叉搜索树的分类操作min max：NeSearchTree（X |Y）->记录。var Rec'：记录。vars L R：SearchTree（X|Y）。变量L ' R'：NeSearchTree（X|Y）。var C '：Y@Contents.mb empty：SearchTree（X |Y）。mb empty [Rec] empty：NeSearchTree（X|Y）。cmb L ' [Rec] empty：NeSearchTree（X|Y）的if key（max（ SearchTree（X|Y）。oplookup：SearchTree（X |Y）X@Elt -> [Y@Contents]。操作删除：SearchTree（X |Y）X@Elt-> SearchTree（X|Y）。eq insert（empty，K，C）= empty [key：K，contents：C] empty. eq insert（L [Rec，key：K，contents：C] R，K，L [Rec，key：K，contents：combine（C，C ' ） ] R .ceq insert（L[Rec]R，K，C）=insert（L，K，C）[Rec] R if K

下载后可阅读完整内容，剩余1页未读，立即下载