Maude功能模块的声明式调试器: 一个隶属方程逻辑的构造器

理论计算机科学电子笔记238（2009）63-81www.elsevier.com/locate/entcsMaude函数模的一个声明式构造器R. Caballero，N. Mart 's-Oliet，A. Riesco和A. VerdejoFacultaddeInforma′tica，西班牙马德里孔普卢顿大学摘要本文提出了一种用于Maude功能模块的声明式调试器，该调试器对应于隶属方程逻辑中的可执行规范。从一个错误的计算开始，声明式调试建立一个调试树作为计算的逻辑表示，然后通过向外部oracle提问来遍历该树，直到发现错误。我们总结了面向等式和成员推理的调试树的构造，其中所有正确性不需要任何证明的节点都被折叠。 Maude的响应特性允许我们生成 并使用Maude本身的操作导航Maude计算的调试树;甚至声明式调试器的用户界面也可以通过这种方式指定。我们提出了调试器关键词：声明式调试，隶属方程逻辑，Maude，功能模块，元级实现1介绍Maude是一种高级语言和高性能系统，支持等式和重写逻辑[12]计算，适用于广泛的应用。特别地，Maude功能模块对应于隶属方程逻辑（MEL）[2，13]中的规范，除了方程之外，还允许描述一个排序元素的隶属断言的声明。通过这种方式，Maude使得数据类型（如排序列表或搜索树）的忠实规范成为可能，这些数据类型的数据不仅通过构造函数来定义，而且还通过满足附加属性来定义。Maude系统支持几种调试Maude程序的方法：跟踪，术语着色，以及使用内部调试器[7，第10章]。 22]。 跟踪由教育部西班牙项目DESAFIOS（TIN 2006 -15660-C 02 -01）和MERIT- FORMS（TIN 2005 -09027-C 03 -03）以及马德里社区方案PROMESAS（S-0505/TIC/0407）支持的研究。1571-0661/© 2009 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2009.05.01364R. Caballero等人/理论计算机科学电子笔记238（2009）63工具允许我们跟踪一个指定的执行，也就是序列的重写。术语着色包括使用不同的颜色进行打印，操作员用于构建不完全减少的术语。Maude调试器允许用户通过选择一些运算符或语句来定义执行中的断点。当找到断点时，进入调试器。在那里，我们可以看到当前项，并在跟踪打开的情况下执行下一次重写Maude调试器有一个缺点，因为它是基于跟踪的，它向用户显示通过使用单个语句获得的每一小步。 因此，用户可以放松对产生错误结果的不正确推理的证明的一般看法。也就是说，当用户检测到意外的语句应用时，很难知道不正确的推断从哪里开始。基于语言语义的不同调试方法E. Y. [19]这是本书的框架。声明式调试已广泛应用于逻辑[10，14，22]、函数[21，17，16，18]和多范式编程[5，3，11]语言。声明式调试是一种半自动技术，它从用户认为不正确的计算（错误症状）开始，并定位导致错误的程序片段声明式调试方案[15]使用调试树作为计算的逻辑表示树中的每个节点代表一个计算步骤的结果，该计算步骤必须通过某种逻辑推理从其子节点的结果得出通过遍历调试树进行诊断，向外部oracle（通常是用户）询问问题，直到找到所谓的buggy节点。buggy节点是包含错误结果的节点，但其子节点都有正确的结果。因此，有缺陷的节点从正确的输入产生了错误的输出，并且对应于错误的代码片段，这被指出为错误。在调试过程中，用户不需要从操作上理解计算。任何有错误的节点都代表一个错误的计算步骤，调试器可以显示负责它的程序片段。从解释的角度来看，声明式调试可以被描述为由两个阶段组成，即调试树生成和遵循一些合适的策略的导航[20]。在这里，我们提出了一个声明式调试器的Maude功能模块[7，章。4]。调试过程开始于从初始项到一个完全减少的意外。我们的调试器在为该推断构建证明树之后，将向用户提出以下形式的问题：“ T完全简化为TJ？"，一般来说，这更容易回答。此外，由于问题位于证明树中，因此答案允许调试器丢弃问题的子集，从而引导和缩短调试过程。该工具的当前版本具有以下特征：• 它支持所有类型的功能模块：运算符可以用任何axiom属性的组合来声明（除了属性strat，它允许R. Caballero等人/理论计算机科学电子笔记238（2009）6365指定评估策略）;等式可以用否则定义属性;模块可以参数化。• 它提供了两种遍历调试树的策略：自顶向下，即从根开始遍历树，每次询问 当前节点，然后继续其中一个不正确的子节点;划分和查询，每次选择子树大小最接近的节点 将整个树的大小减半，如果其根不正确，则仅保留该子树，否则删除整个子树• 在开始调试过程之前，用户可以选择一个只包含正确语句的模块。通过检查关于该模块的推断的正确性（即，使用该模块作为Oracle），调试器可以减少向用户询问的问题• 它允许用户调试Maude功能模块，其中一些方程和成员关系是可疑的，并已标记（每个都有不同的标签）。只有这些标记的语句才会在证明树中生成节点，而未标记的语句则被认为是正确的。用户负责该标签。此外，用户可以回答他信任与当前被质疑的推断相关联的语句;也就是说，语句可以被“完全”信任Maude利用重写逻辑是反射性的这一事实[6，8]，其一个关键的区别特征是通过其预定义的META-LEVEL模块[7，Chap.这个特性使得Maude具有显著的可扩展性，并允许许多高级元编程和元语言应用程序。这个强大的功能允许访问元级实体，如规范或计算作为通常的数据。因此，我们能够使用Maude本身的操作生成和导航Maude计算的调试树。此外，Maude系统还提供了另一个模块，LOOP-MODE[7，Chap. 17]，其可用于指定与用户的输入/输出交互。因此，我们的声明式调试器Maude功能模块，包括其用户交互，在Maude本身实现关于声明式调试方法的基本原理、其他示例以及有关实现的更多信息的完整解释可 以 在 技 术 报 告 [4] 中 找 到 ， 该 报 告 与 调 试 器 的 Maude 源 文 件 一 起 可 以 从http://maude.sip.ucm.es/debugging网站获得。2Maude功能模块正如在引言中提到的，Maude使用了成员关系方程逻辑[2，13]，这是一种非常有表现力的方程逻辑版本，除了方程之外，还允许描述一个排序元素的成员关系断言。我们在下面介绍它的规格如何表示为Maude功能模块，并简要描述了我们的调试器的理论基础66R. Caballero等人/理论计算机科学电子笔记238（2009）63不∀⇐↓∈→→∈∀⇐ ∧∧{}{}∈×一|→A|2.1隶属方程逻辑MEL中的签名是一个三元组（K，S，S）（在下文中仅为K），其中K是一组类型，太空一号... kn，k（k1. kn，k）KK 一个多类签名，S=SKk∈K是两两不相交的K-类集合族.直观地说，有kind但没有sort的术语表示未定义或错误的元素。 MEL原子公式可以是等式t=tJ，其中t和tJ是相同种类的项，也可以是t：s形式的成员关系断言，其中项t具有种类k，而s Sk。句子是形式为（X）A0A1.. An，其中每个Ai要么是一个方程，要么是一个成员断言。排序符号s1 Nat.在逻辑上理解为一种类型级别的声明op _div_：[Nat] [Nat] -> [Nat].以及条件成员公理如果N：Nat和M：NzNat，则cmb N div M：Nat。子排序声明NzNat Nat在逻辑上被理解为条件成员公理如果N：NzNat，则cmb N：Nat。2.2.1一个例子：二叉搜索树作为Maude功能模块的一个例子，我们展示了如何指定没有重复元素的二叉搜索树，其节点包含满足理论STOSET（定义它们的严格全序）的元素[7，Sect.8.3]。fmod搜索树{X：： STOSET}是排序NeSearchTree{X} SearchTree{X} Tree{X}。子排序NeSearchTree{X} SearchTree{X}[ctor].操作 ：Tree{X} X$Elt Tree{X} -> Tree{X}[ctor]。其中用于构建非空搜索树的操作使用并置，X$Elt表示来自理论STOSET的排序Elt。当一棵树的根大于左子树中的所有元素，小于右子树中的所有元素时，它就是一棵搜索树;这个要求通过成员资格来指定。假设子树是搜索树，而不是与它们的所有元素进行比较，与适当子树的最小值或最大值进行比较就足够了变量E E '：X$Elt.vars L R：SearchTree{X}. 变量L ' R'：NeSearchTree{X}。mb[leaf]：empty E empty：NeSearchTree{X}.cmb [1ch1]：L' E empty：NeSearchTree{X} if max（L'）E<.cmb [1ch2]：empty E R<'：NeSearchTree{X} if E min（R'）. CMB[2CH] ：L如果max（< X$Elt.ceq [mn1]：min（empty E R）= Eifempty E R：NeSearchTree{X} . ceq[mn2]：min（L′ E R）= min（L ′），如果L ′ E R：NeSearchTree{X}。ceq [mx1]：max（L E empty）= E if L E empty：NeSearchTree{X} . ceq [mx2]：max（L ER' ） = m a x （ R ' ） ，如 果 L E R ' ： N e S e a r c h T r e e { X } 。删除操作通常通过结构归纳来指定，在非空的情况下，通过比较要删除的元素与树根来指定根据前者是否小于，68R. Caballero等人/理论计算机科学电子笔记238（2009）63我→我我| →我|→等于或大于后者。操作删除：SearchTree{X} X$Elt->SearchTree{X}。EQ[dl1] ：delete（empty，E）= empty.ceq [dl2]：delete（LE R， red delete（（empty 1 empty）2（（empty 4 empty）5（empty 6（empty 7empty），5）. 结果NeSearchTree{Int}：（空1空）2（（空4空）6（空6（空7空）我们得到一棵有重复的树。此外，Maude推断这是一棵搜索树！ 你注意到虫子了吗？ 我们将在3.3节中展示如何使用调试器来探测它们。2.3声明式调试可以找到定义操作语义的演算的推理规则 如图1所示。它们是对文献[2]中提出的MEL演绎规则的Maude函数模情况的一种适应。我们假设存在对规范的预期解释，这是一个与用户在编写语句E时所考虑的模型相对应的代数。用户期望对于计算的每个约简eeJ和隶属度e：s，w.r.t.规格（E）。我们会说e eJ（分别是e：s）在它成立时有效，否则无效声明式调试器依赖于某些外部oracle（通常是用户），以便获得有关调试树中某些节点的有效性的信息有效性的概念可以扩展到区分错误的方程和错误的成员公理，这些特定的片段可以从有效信息中推导出将演算中的演绎表示为证明树将是方便的，其中前提是每个推理步骤中结论的子节点。在声明式调试中，我们对有缺陷的节点特别感兴趣，这些节点是无效节点，其所有子节点都是有效的。我们的目标是在以用户检测到的初始错误症状为根的任何证明树T中找到一个有缺陷的节点。这可以简单地通过根据以下自顶向下策略向用户询问关于树中节点的有效性的问题来完成：输入：一个树T，它有一个无效的根。R. Caballero等人/理论计算机科学电子笔记238（2009）6369e：一|--AA |→A→（Re）e→e（Rf）（传递性）e1→eJeJ→e2（Tr）e1→e2（同余）e1 → EJ1.en→ eJnf（e1，.， en）→ f（eJ1，.，（e、J、n）（主题缩减）e→eJeJ：s（SRed）（丛）（隶属度）{θ（ui）↓θ（uJi）}1≤i≤n{θ（vj）：sj}1≤j≤mθ（e）：s（Mb）如果e：s<$u1=uJ1<$··<$un=uJn<$v1：s1<$··<$vm：sm（置换）{θ（ui）↓θ（uJi）}1≤i≤n{θ（vj）：sj}1≤j≤m（Rep）如果J=Jθ（e）→θ（eJ）J ：：e→ε1u1···un=unv1s1· ··vmsmFig. 1. Maude函数模输出：T中的错误节点。说明：考虑T的根N。 有两种可能：• 如果N的所有子元素都是有效的，则最终将N标识为错误的。• 否则，选择以任何无效子节点为根的子树，并递归地使用相同的策略来查找错误节点。证明这个策略是完备的，可以直接在T的高度上使用归纳法。因此，如果T是一个具有无效根的证明树，则存在一个有缺陷的节点N∈T，使得N的所有祖先都是无效的。然而，我们将不使用证明树T作为调试树，而是使用合适的缩写，我们用APT（T）表示（来自缩写证明树）。 为了 为了简化证明树，我们利用了每个代数都满足的一个性质：如果e eJ（分别为e：s）可以由微积分的前四个推理规则中的任何一个使用成立的前提推导出来，那么=eeJ（分别为e：s）。这个性质不能扩展到成员和替换推理规则，其中结论的正确性不仅取决于微积分，还取决于相关的指定语句，这可能是错误的。因此，唯一能从有效前提得到无效结论的推论，即， 唯一可能的故障节点对应于替换和成员资格推断。APT（T）仅保留与这些推断相对应的节点。 图2显示了APT（T）的定义，其中Ti表示证明树对应的前提在一些推论。规则APT1保持根不变，并采用辅助函数APTJ来产生子树。 APT J定义在规则APT 2中。 APT 8. 它 接受一个证明树作为输入参数并返回一个森林T1，.Tn的APT作为结果。假设自上而下尝试APTJ的规则，特别是如果APT3也适用，则不得应用APT4 很容易检验替换或隶属推理的每个节点N ∈ T结论都有其对应的节点NJ∈ APT（T）标记为相同的缩写，反之，对于70R. Caballero等人/理论计算机科学电子笔记238（2009）63@3（SRed）7（Mb）8（重复）→我∈∈→→6→→e：s12.不... T！APTJ.T1.. . Tn（R）！（APT1）APT1N（R）=afaf（with（R）any inference rule）af（APT2）AP T J. e→e（Rf）！=0BT1. . . Tn（重复）C1（APTJ（T1）. . . APTJ（Tn）APTJ（Tn+1））T=（APT）APTJe1→eJe1→e2n+1（Tr）Ae1→e2（Rep）（APT）APTJ.T1T2（Tr）！={AP T J（T），AP T J（T）}4 1 2e1→ e2（APT）AP T J.T1... Tn ！={AP T，J（T），.， AP T J（T）}（丛）5 1ne1→ e2（APT）AP T J.T1T2！={AP T J（T），AP T J（T）}（APT）APTJ.T1.. . Tn ！=（APTJ（T1）.. . APTJ（Tn）（Mb））e： s e： s（APT）APTJ.T1.. . Tn！=（APTJ（T1）.. . APTJ（Tn）（Rep））e1→ e2e1→ e2图二、获得简化证明树的转换规则每个NJAPT（T）与根不同，存在节点NT，也就是 替换或成员推理的结论。特别地，与APT3的右侧中的e1e2相关联的节点是证明树T的节点e1eJ，其不包括在APT（T）中我们选择在APT（T）中引入e1e2而不是简单地引入e1ej，作为简化APTs结构的实用方法，因为e2是从eJ获得的，因此可能更简单（APT3中的树Tn+1的根必须是必要的形式eJe2，这是根据图1中的传递性推理规则的结构①的人。虽然APT（T）不再是证明树，但我们保留了推理标签（Rep）和（Mb），隐含地假设它们包含对原始证明树中相应步骤使用的等式或成员公理的引用。调试器使用此信息来挑出指定代码的不正确片段。树的缩写减少和简化了将被问到用户的问题，同时保持了技术的可靠性和完整性，如下面的定理（在[4]中证明）所保证的：定理2.1设S是一个指定，它的预期解释，T是一个有无效根的有限证明树。然后又道：• APT（T）包含至少一个有缺陷的节点（完整性）。R. Caballero等人/理论计算机科学电子笔记238（2009）6371叶▲4▲：NeSTmx1叶▲7▲：NeSTmn1叶min（▲7▲）→71ch2▲7▲：NeSTmx1▲6（▲7▲）：NeSTmax（▲7▲）→7mx2叶max（▲4▲）→4max（▲6（▲7▲））→7\r2ch\ //下一页▲1▲：NeSTmax（▲1▲）→1MX1（▲4▲）6（▲6（▲7▲））：NeST（*）max（（▲4▲）6（▲6（▲7▲）→72ch\/MX2（▲1▲）2（（▲4▲）6（▲6（▲7▲）：NeST图三. 简化证明树• APT（T）中的任何错误节点在S（可靠性）中具有相关联的错误语句。该定理指出，我们可以安全地使用简化的证明树作为Maude功能模块的声明式调试的基础：该技术将从用户检测到的任何初始症状开始查找错误节点。当然，这些结果假设用户正确回答了调试器询问的关于APT节点有效性的所有问题（参见第11节）。3.1）。2.2.1节中错误成员推断的APT如图3所示，其中▲表示空搜索树，Q表示已经描述过的证明子树，其中r ootmax（▲6（▲7▲））→7。3使用调试器在描述用户与调试器交互的基础知识之前，我们解释了用户引入的模块的假设;然后我们介绍了可用的命令以及如何使用它们来调试第节中介绍的错误示例。2.2.1.3.1假设由于我们正在调试Maude功能模块，因此期望它们满足适当的可执行性要求，即，规格必须是终止的，连续的和排序递减的。我们的工具的一个有趣的功能是，用户可以信任一些语句，通过标签应用到可疑的语句。 这意味着未标记的语句被假定为正确的。可信语句在实现中被视为图1中的前四个规则在APT转换中被处理;更具体地说，对应于可信语句的成员资格或替换推理规则的实例在缩写证明树中被折叠。为了获得一个非空的简化证明树，用户必须标记一些语句（所有的都有不同的标签）;否则，一切都被认为是正确的。特别是，有错误的语句必须被标记才能被发现。当不是所有的语句都被标记时，2.3节中所示的正确性和完整性结果取决于用户负责的标记的良好性。虽然用户可以引入一个模块导入其他模块，调试过程发生在被调用的模块中。但是，调试器允许72R. Caballero等人/理论计算机科学电子笔记238（2009）63用户信任整个导入模块。如前所述，调试树的导航是通过向外部oracle提问来实现的，在我们的例子中，外部oracle是用户或用户引入的另一个模块。在这两种情况下，答案都被认为是正确的。 如果模块不是真正正确的，或者用户提供了一个不正确的答案，结果是不可预测的。请注意，正确的模块提供的信息不需要是完整的，因为某些函数只能部分定义。3.2命令调试器在Maude中通过加载文件fdd.maude启动，它启动一个输入/输出循环，允许用户与工具交互正如我们在介绍中所说，生成的证明树可以使用两种不同的策略进行导航，即自顶向下和划分和查询，后者是默认策略。用户可以使用命令在它们之间切换（自顶向下策略）。和（divide-query strategy.）. 如果使用具有正确定义的模块来减少问题的数量，则必须在使用命令（正确的 模块MODULE-NAME）开始调试之前指出。.用户可以选择在调试过程中使用所有带标签的语句（默认情况下），或者通过命令选择其中的一些(set debug select on.）激活此模式后，用户可以使用（调试选择标签。）（调试标签。）其中LABELS是由空格分隔的标签列表此外，可以使用以下命令选择或取消选择已删除模块的语句中的所有标签：（调试包括模块。）（调试排除模块。）其中MODULES是由空格分隔的模块名称列表。一旦我们选择了策略和（可选）正确的模块和可疑标签，我们就用命令1开始调试过程（debug[inMODULE-NAME：]INITIAL-TERM->WRONG-TERM.）同样，我们可以使用以下命令调试成员资格推断（debug[inMODULE-NAME：]INITIAL-TERM：WRONG-SORT.）这个过程如何继续取决于所选择的策略。如果选择自上而下的策略，每个问题中将显示多个节点 如果有一个无效的节点，我们必须使用命令（nodeN）选择其中一个。其中N是错误节点的标识符。如果所有的节点都是正确的，我们输入（all valid）。. 在划分和查询策略中，每个问题都涉及一个可能正确或错误的推断。不同的答案被传输到1如果没有给出模块名称，则默认使用当前模块R. Caballero等人/理论计算机科学电子笔记238（2009）6373叶▲4▲：NeSTmx1叶▲7▲ ：NeSTmn1叶min（▲7▲）→71ch2▲7▲：NeSTmx1▲ 6（▲7▲）：NeSTmax（▲7▲）→7mx2max（▲4▲）→4max（▲ 6（▲7▲））→7（†）2ch（▲4▲）6（▲ 6（▲7▲））：NeST见图4。 第一个答案叶▲4▲：NeSTmx1max（▲4▲）→42ch（▲4▲）6（▲ 6（▲7▲））：NeST图五. 第二个答案调试器与命令（是的。） 和（不）. 除了回答“是”之外，我们还可以相信一些声明，如果一旦进程开始，我们确定bug不存在。 要信任当前语句，我们键入命令（trust.）.最后，我们可以使用命令（undo）返回到两种策略中的前一个状态。.3.3二叉搜索树我们从Sect。2.2.1我们的二叉搜索树规范中的删除是不正确的。特别是Maude将排序NeSearchTree{Int}分配给具有重复的树。我们可以使用以下命令Maude>（在搜索树测试中调试：（empty1 empty）2（（empty 4 empty）6（empty 6（empty 7 empty）：NeSearchTree{Int}.）它通过将所有标记语句视为可疑语句来生成图3由于默认的导航策略是划分和查询，调试器选择图中标有*的节点，然后询问以下问题：此成员资格（与成员资格2ch相关联）是否正确？（empty4empty）6（empty 6（empty 7 empty））：NeSearchTree{Int}Maude>（no.）由于答案是否定的，调试器将丢弃树的其余部分，并将焦点放在以该节点为根的子树中（参见图4）。 下一个问题对应于图中标有†的节点。这个转变（与方程mx2相关）正确吗？max（empty 6（empty7 empty））->7Maude>（yes.）当答案是肯定的，相应的子树被删除，在这种情况下获得图中的树五、接下来的问题是这个转变（与方程mx1相关）正确吗？max（empty 4empty）->4Maude>（trust.）在最后一个问题中，我们意识到应用的方程非常简单，74R. Caballero等人/理论计算机科学电子笔记238（2009）63- -\/\ // \ // \ //下一页\/\/1ch2\/2通道\/dl2\/2通道▲6（▲7▲）：NeSTR：NeSTdl（▲6（▲7▲），5）→▲6（▲7▲）dl6（▲1▲） 2R：NeSTdl（R，5）→（▲4▲） 6（▲6（▲7▲））dl3dl（（▲1▲） 2R，5）→（▲1▲） 2（（▲4▲） 6（▲6（▲7▲）见图6。 自顶向下策略这个答案的行为类似于yes：它会删除根被标记为当前语句的所有子树。 有了这些答案，我们得到一个 树中只有一个节点，调试器能够得出结论，这是错误的成员资格。错误节点是：（empty 4 empty）6（empty 6（empty 7 empty））：NeSearchTree{Int}带有关联成员：2ch事实上，如果我们现在检查这个成员关系，我们会注意到它将根与右子树的最大值进行比较，而它应该与最小值进行比较。修复这个错误后，delete函数仍然是不正确的，所以我们调试这个函数（为了说明起见，使用自顶向下的策略Maude>（自上而下策略。）选择自上而下的策略。Maude>（将debug select设置为on。）已启用“选择”。Maude>（debug select leaf 1ch1 1ch2 2ch dl2 dl3 dl4 dl5 dl6.）标签leaf 1ch1 1ch2 2ch dl2 dl3 dl4 dl5 dl6现在可疑。Maude>（在搜索树测试中调试：delete（（empty 1 empty）2（（empty 4 empty）5（empty 6（empty 7empty））），5）->（空1空）2（（空4空）6（空6（空7空）））。）在这里我们决定把成员关系和非平凡的删除方程标记为可疑。在这种情况下，调试器构建图1所示的证明树（部分）。6（其中R表示search树（▲4▲）5（▲6（▲7▲），所以它会问以下问题：请选择一个错误的节点：节点0：（empty 1 empty）2（（empty 4 empty）5（empty 6（empty 7 empty）：NeSearchTree{Int}节点1： delete（（empty 4 empty）5（empty 6（empty 7 empty）），5）->（empty 4 empty）6（empty 6（empty 7empty））Maude>（node 1.）请选择一个错误的节点：节点0：空6（空7空）：NeSearchTree{Int}节点1：（empty 4 empty）5（empty 6（empty 7 empty））：NeSearchTree{Int}节点2：delete（empty 6（empty 7 empty），5）-> empty 6（empty7 empty）Maude>（allvalid.）错误节点是：delete（（empty 4 empty）5（empty 6（empty 7 empty）），5）->（空4空）6（空6（空7空））调试器得出结论，问题在等式dl6内。我们把修复它的任务留给感兴趣的读者R. Caballero等人/理论计算机科学电子笔记238（2009）63754执行正如我们在介绍中所说的，Maude的响应能力允许我们在Maude本身中生成和导航计算的调试树。由于导航是通过向用户提问来完成的，因此这个阶段必须处理导航策略以及与用户的输入/输出交互。事实上，这种交互也可以在Maude中通过使用预定义的模块LOOP-MODE[7，Chap. 17]，它处理输入/输出并维护工具的持久状态。下面我们展示了实现中涉及的主要功能;技术报告[4]提供了完整实现的完整解释，包括用户交互。4.1树形结构为了构建调试树，我们使用Maude函数模块中定义的方程既终止又连续的事实。我们不是先创建完整的证明树，然后再将其简化，而是直接构建简化的证明树。保存在每个节点中的信息对应于一个推理，由语句的标签、其左侧（项）和其右侧（术语或排序）。函数APT Tree控制该树的构造（它实现图2中的函数APT）。它接收发生可疑推断的模块、用于修剪树的正确模块（或者当没有提供这样的模块时，可以是常数）、最初减少的项、获得的（错误的）结果以及可疑语句标签的集合。 它保持初始约简为根 并使用辅助函数WARNING Forest（实现图2中的函数APTJ），除了WARNING Tree接收的参数之外，该辅助函数还接收可疑语句的模块 作为参数给出的两个项。这个转换后的模块用于提高树构造的效率，因为我们可以使用它来检查一个术语是否达到它的最终形式只使用可信的语句，从而避免建立一个树，最终将是空的。操作树：Module Maybe{Module} Term Term QidSet -> Tree。10.C++（C++）= C+tree（nodeF：= Forest（M，M'，CM，正常（M，T），正常（M，T'），QS）。其中，如果在计算之后树的根被复制，则合约修剪该根的树。我们使用函数CumberForest来创建一个缩写树的森林。此函数检查是否可以通过仅使用受信任语句或如果正确的模块可以计算出这种减少;在这种情况下，没有必要来计算森林。否则，它将使用与76R. Caballero等人/理论计算机科学电子笔记238（2009）63Maude解释器：它首先尝试完全减少子项（通过函数reduceSubterms），一旦所有子项都减少了，如果结果不是最终结果，它尝试在顶部减少（通过使用函数applyEq），通过传递性达到最终结果。操作符Forest：Module Module Maybe{Module} Term Term QidSet ->Forest。ceq森林（OM，TM，CM，T，如果reduce（TM，T）== T '，则-else reduce（M，T）== reduce（M，T'）。ceq森林（OM，TM，CM，T，如果否则F应用Eq（OM，TM，CM，if：= reduceSubterms（OM，TM，CM，T，QS）[owise]。reduceSubterms函数返回一个由完全约简的项及其子项组成的对（也就是说，该函数模仿图1中的同余规则的特定行为）以及由这些约简生成的缩写树森林。函数applyEq试图通过使用图1中的替换规则来应用（在顶部）一个等式2，其中约束是我们不能应用具有否则属性的等式，而可以应用其他等式。为了应用一个方程，我们检查我们试图减少的项是否匹配方程的左侧，并且它的条件是否满足。如果发生这种情况，我们得到一个替换（从与左侧的匹配和匹配条件），我们可以应用到等式的右边。请注意，如果我们可以在正确的模块中获得转换，则不会计算森林op applyEq：Module Module Maybe{Module} Term Term QidSet -> Forest.op applyEq：Module Module Maybe{Module} Term Term QidSet EquationSet -> Forest.ceq applyEq（OM，TM，CM，T，如果reduce（TM，T）== T '，否则reduce（CM，T）==T'。eq applyEq（OM，TM，CM，T，applyEq（OM，TM，CM，T，T ' ， Q S ， g e t E q s （ O M ） ） [ o w i s e ] .首先，我们尝试在没有otherwise属性的情况下应用方程。 另一方面，我们检查其他方程。ceq applyEq（OM，TM，CM，T，(AtS，QS）thentree（node（label（AtS）：T->TFi如果C [AtS]，则L = R。：= generalEq（Eq）/\not owise？(AtS)//\SB：= metaMatch（OM，L，T，C，0）/\RF：= conditionForest（substitute（C，SB），OM，TM，CM，QS）条件Forest（OM，TM，CM，R'，T'，QS）。函数在哪里？ 检查等式Eq是否可疑。 如果是这种情况，则生成与所应用的方程相对应的新节点。条件的森林由函数conditionForest生成;因为它是在2.由于模是连续的，我们可以选择任何方程，最终结果应该是相同的。R. Caballero等人/理论计算机科学电子笔记238（2009）6377在检查了条件是否满足（通过上面的函数metaMatch）之后，它不会再次检查。 它区分了不同类型的条件。如果条件是一个方程，则生成将项归约到其标准形式的树。op conditionForest：Condition Module ModuleMaybe{Module}QidSet -> Forest.eq conditionForest（T =TForest（OM，TM，CM，T