程序切片信息的证明导向调试接口扩展及应用

理论计算机科学电子笔记174（2007）19-33www.elsevier.com/locate/entcs利用程序切片信息路易丝·A 丹尼斯1，2英国诺丁汉大学计算机科学与信息技术学院摘要本文提出了一种扩展定理证明接口与证明导向调试和其他反证为基础的应用程序。该扩展基于跟踪用户识别的规则集，以创建信息丰富的程序切片。根据这些规则在成功和不成功的证明分支中的参与来收集信息这为判断任何规则的正确性提供了一个启发式得分。提出了一个简单的机制，语法突出显示的基础上，这些信息和一个小的案例研究，说明其操作。这些想法尚未付诸实施。保留字：面向证明的编译、程序切片、验证1引言使用验证来定位定理中的错误，更具体地说是程序中的错误，是一个相对被忽视的领域，提供接口来帮助完成这项任务也是如此。本文认为，证明导向调试的功能程序，并提出了一个扩展到目前的定理证明接口，以支持这一点。该扩展是基于这样的假设，即调试过程涉及定位程序语句，或者在函数程序的情况下，定位不正确的函数情况。这个不正确的语句将出现在程序切片中，可以在验证过程中识别。在证明过程中也可以识别导致正确演绎的其他程序片段。这些信息可以用来在接口中创建适当的语法高亮。提出了一种潜在的突出显示方案，并基于Isabelle/HOL [12]和ProofGeneral [1]进行了一个简单的案例研究，以说明这是如何工作的。1本研究由EPSRC赠款GR/S 01771/01和诺丁汉NLF赠款3051资助。2电子邮件：lad@cs.nott.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.09.01920洛杉矶Dennis/Electronic Notes in Theoretical Computer Science 174（2007）尚未实施，但在Isabelle Proof General的背景尽管本文中的讨论是基于证明导向调试的应用程序，但类似的机制可能也适用于需要识别证明失败原因的其他情况本文的组织如下：§2讨论了证明导向的调试和程序切片的概念;§3提出了一种通过证明跟踪程序切片的机制，§ 4通过一个简单的案例研究给出了这种机制的例子;§5讨论了在自动化系统中使用类似机制的一些结果;§6看了一些相关的工作，§7讨论了实现问题和其他进一步的工作。2有向证明与程序切片证明导向的调试首先由Harper [10]提出，目前正在进行工作，将其扩展为通过证明过程定位程序错误的框架[6]。使用框架而不是依赖于用户在一般证明方面的技能的想法程序调试构造了一个程序在某个输入上运行的执行树，然后在每次树分支时询问用户。这会识别出返回错误结果的分支，从而定位导致错误的代码段。程序切片最早是由Weiser提出的[17]。其核心思想是在程序中的某个点上识别出一个感兴趣的变量（称为切片标准），然后提取程序的一个片段（程序切片），该片段要么包含该点上变量值所依赖的所有语句，要么包含该点上变量值所依赖的片段。命令式语言的程序切片技术通常遵循这项工作[16]，使用控制流图，数据流图或其他基于图的程序表示，其中语句表示为图中的节点，程序切片表示为图中的一组节点。在函数式程序中，函数应用代替了程序语句.切片准则的概念也可以推广（例如[14]中的投影）。证明导向的调试背后的意图是使用证明的分支显然需要提供适合这项任务的适当工具（即战术/会计标准专家组方法）。本文不集中在这方面，但考虑，而不是一个定理证明器的接口可以通过相关的程序片的演示文稿来帮助用户的方式3证明树分支作为切片标准函数式程序的验证自然涉及到将程序分解为一组等式规则，每个规则对应于其函数定义中的一个情况。因此，可以跟踪这些规则在证明中的使用，从而有效地创建程序洛杉矶Dennis/Electronic Notes in Theoretical Computer Science 174（2007）21切片（即，在任何程序的证明中使用的程序的那些部分），以及保持的指示证明的多少真分支和假分支使用了该规则的“分数”（通常作为简化过程的一部分）。这些分数然后可以由界面使用以向用户返回附加信息为了简单起见，我们将继续把这些规则轨迹称为程序切片，即使在定理证明的上下文中，没有理由不把它们作为与任何程序无关的定义、引理和定理的让我们考虑一个用ML编写的简单插入排序程序。funinsert x [] =[x]| 插入x（h：：t）=如果x≤ h，则 x：：h：：telseh：：insert t;funsort [] =[]| sort（x：：xs）= insert x（sort xs）;定义的每种情况都成为四个等式规则之一：(i) 插入x [] =[x](ii) insert x（h：：t）= if x≤h then x：：h：：telse h：：insert x t(iii) sort [] =[](iv)sort（x：：xs）= insert x（sort xs）我们建议，一个证明导向的调试界面应该允许用户在验证尝试期间将这些定义中的一个选择指定为“可疑”。显然，用户可以选择将其开发中涉及的所有定义命名为可疑定义，包括与规范相关的定义，甚至是来自定理证明器的理论数据库的预先存在的定义，一旦实现了这样的接口，这显然是一些实验研究的主题。我们假设一个定理证明系统生成一系列的证明状态，其中，至少，包含列表中的当前开放的目标在证明尝试。其中心思想是将程序切片与这些证明状态中的目标相关联。证明状态中的每个目标g与一组可疑规则（切片）S（g）相关联，这些可疑规则已在该目标的推导中使用此外，该系统也在每个证明状态s中存储一组三元组，将每个可疑规则r与两个整数相关联，其中第一个整数是好整数good（r，s），每当证明分支关闭时（因为它已被成功证明），第二个整数是坏整数bad（r，s），每当目标得出假结论时（如果随后在假设中发现矛盾，则可以修改）。在很明显的地方，状态参数将从这些函数中删除。这两个分数可以用来形成规则正确的概率估计。对于所有规则r，初始好（r）和坏（r）被设置为零，并且初始目标gi与空程序切片S（gi）= []相关联。随着证明的进展，系统更新信息如下：考虑两个证明状态，sn后跟sn+1。 sn+1由sn通过a22洛杉矶Dennis/Electronic Notes in Theoretical Computer Science 174（2007）用一组子子目标替换一些父目标的策略测试。对于每一个新的子目标g，在这样一个证明状态中，父目标gp。• 设R是t从gp导出g所使用的可疑规则集，S（g）=S（gp）<$R。• 如果g有一个假结论，而gp没有，那么对于S（g）中的所有规则r，bad（r，sn+1）=bad（r，sn）+1.•如果g有真结论，则对于S（g）中的所有规则r，good（r，sn+1）=good（r，sn）+1. 此外，如果g p的结论为假，则bad（r，s n+1）= bad（r，s n）−1。这最后一个修改允许一个假目标成为封闭的（通过发现假设中的矛盾），然后纠正坏整数，以抵消前面对假的推导所产生的结果。• 对于所有剩余的规则，r，good（r，sn+1）=good（r，sn）和bad（r，sn+1）=bad（r，sn）.总的来说，如果接口承担跟踪规则使用信息的任务，而不是底层的定理证明器，因为这些信息是额外的逻辑，那么这似乎是更可取的。然而，在自动化或半自动化系统中，如证明计划器（例如IsaPlanner [8]和λClam[13]），在证明系统本身中跟踪这些信息似乎是有益的，以便它可以通知自动调试过程[5]。向用户呈现此跟踪信息的明显机制是与每个目标相关联的语法突出显示的规则列表。例如，本文将使用表1所示的单色约定。类别有突出显示公约r∈ S（g）bad（r）> good（r）坏（r）<好（r）大胆强调斜体表1本文中使用的突出显示约定之所以选择这些报告，是因为在下文讨论的例子中，这些报告提供的信息最多。被解释为用于导出此目标，可能是错误的，也可能是正确的。原则上，没有理由将这种突出限制在三个类别。 事实上，在一个 自动化系统，我们在§5中主张基于排序的另一类坏整数和好整数的元组。4为例我们现在展示一些在Isabelle/Isar系统中进行的不正确定理的证明尝试的例子[12，18]。这些例子来自一个有缺陷的学生ML程序的语料库[7]。我们将考虑图1所示的ML程序的验证。这洛杉矶Dennis/Electronic Notes in Theoretical Computer Science 174（2007）23funinsert x [] =[]| 插入x（h：：t）=如果x≤ h，则 x：：h：：telseh：：insert t;funsort [] =[]| sort（x：：xs）= insert x（sort xs）;FunOnce [] =[]| 一次（x1：：x2：：xs）=如果x1 = x2，则一次（x2：：xs）elsex1：：x2：：Once xs;funonceOnly [] =[]| onceOnly（x：：xs）= Once（sort（x：：xs））;Fig. 1. 一个有缺陷的ML程序普里姆雷克insert_nil：“insert x [] =[]”insert_cons：“insert x（h#t）=（if x≤ h thenx#h#t else h#insert x t）”普里姆雷克sort_nil：“sort [] =[]”sort_cons：“sort（x#xs）= insert x（sort xs）”recdefOnce“measurelength”once_nil：“Once []=[]”once_cons：“一次（x1#x2#xs）=（如果x1=x2，则一次（x2#xs）else x1#x2#Once xs）”普里姆雷克onceOnly_nil：“onceOnly [] =[]”onceOnly_cons：“onceOnly（x#xs）= Once（sort（x#xs））”图二. Isabelle Buggy计划是一个真实的例子，由一个学生提交，作为一个练习的解决方案，一个函数onceOnly，当应用于列表l时，返回一个新列表，其中只包含l中每个元素的一个副本。这个程序有三个错误。首先，插入函数的基本情况不正确。其次，在Once函数的定义中缺少一个case（长度为1的列表的case），最后在递归case的else分支中，表达式应该是x1：：Once（x2：：xs）。图2显示了取自[ 7 ]的学生程序的Isabelle形式化应该注意的是，这代表了ML到Isabelle中的一个幼稚的浅嵌入，但这是在这种规模下进行证明导向的调试的一个足够。为了验证这个程序，使用了另一个函数count_list，它计算第一个参数在第二个参数中出现的次数。需要证明的第一个定理是：<$x∈l= n个计数列表x（onceOnly l）= 0在本案例研究中，我们假设insert、sort、Once和onceOnly的定义都被认为是可疑的，这给了我们八个可疑规则： insert_nil、insert_cons、sort_nil、sort_cons、once_nil、once_cons、onceOnly_nil和onceOnly_cons。我们还假设以下定理已被证明：(1)onceOnly l=一次（排序l）本节的其余部分组织如下。 §4.1示出了切片cre。在证明的初始阶段，为了给出信息更新如何工作的概念，§4.2说明了达到错误目标的后果，§4.3说明了24洛杉矶Dennis/Electronic Notes in Theoretical Computer Science 174（2007）当案件丢失4.1基本用法下表显示了在初始校样状态规则好坏规则好坏插入零插入孔0000Once_nil一旦_缺点0000sort_nil排序条件0000onceOnly_nilonceOnly_cons0000从现在开始，我们将省略完整的表，而是集中精力总结可以通过语法突出显示提供的信息。在证明的开始有一个伊莎贝尔的目标1. <$x∈l=0count_list x（onceOnly l）= 0其上附着有空切片。从表象上看，似乎最好省略任何定义未出现在当前目标中的常数的规则，因此初始目标将显示额外的信息（注意。目前，这些规则不属于表1所述的任何类别，因此也没有以任何方式突出显示）：•“onceOnly [] =[]”•“onceOnly（x#xs）=一次（sort（x#xs））”证明尝试通过简化、替换只有一次，一次（排序l），根据（1），然后对列表3应用长度归纳。由于（1）不在我们的可疑列表中，因此没有记录它在简化中的使用。我们同样，它需要对实现进行实验，以确定这是否是一个明智的选择。这给了我们以下伊莎贝尔的目标：1. ！！xs. [|是的长度ys长度xs→ <$ x∈ ys→count_list x（Once（sort ys））= 0;<$x ∈ xs|]=计数列表x（一次（排序xs））= 0这引入了两个新的可疑常数，但到目前为止还没有使用我们的规则。此外，常量onceOnly不再被提及，因此其定义规则从显示列表中删除。因此，建议产出如下。•“sort [] =[]”•sort（x#xs）= insert x（sort xs）[3]选择长度归纳法作为合适的证明方案需要对这些类型的证明有一定的经验。 目前，这项工作假定用户具有相对复杂的定理证明能力，但矛盾的是，相当天真的程序调试技能洛杉矶Dennis/Electronic Notes in Theoretical Computer Science 174（2007）25•“一次[] =[]”•“一次（x1#x2#xs）=（如果x1=x2则一次（x2#xs）else x1#x2#Once xs）”下一步是使用Isarcases方法对xs进行案例分割，然后立即简化所有目标。这会自动释放与案例分割相关的第一个目标（对于xs=[]），让我们只剩下一个目标：1. ！！一份名单xs = a # list=count_list x（Once（insert a（sort list）= 0释放第一个目标创建了一个由sort_nil和once_nil组成的切片，并更新了好整数，使得good（sort nil）= good（once nil）= 1。剩下的目标是使用规则sort_cons生成的，因此它的切片是[sort_cons]。因此，遵循语法高亮约定，我们得到以下规则注释：•“插入x [] =[]”•“insert x（h#t）=（if x h then x#h#t else h#insert x t）”•“sort [] =[]”•sort（x#xs）= insert x（sort xs）•“一次[] =[]”•“一次（x1#x2#xs）=（如果x1=x2则一次（x2#xs）else x1#x2#Once xs）”我们已经看到了关于程序切片的信息，我们可以有一些信心，我们得到了一些与当前目标相关的切片信息4.2推断错误很明显，在尝试上述证明时，需要建立一些关于排序函数的独立这提供了一个很好的例子，说明当目标评估为False时系统的行为。让我们考虑一个简单的引理来证明列表l的所有成员也是排序l的成员。我们从目标开始：定理“x∈ l=<$ x∈（sort l）”根据我们以前的规则和指导方针，显示的规则是：•“sort [] =[]”•sort（x#xs）= insert x（sort xs）证明继续通过l上的长度归纳（这不会改变an-符号），然后是xs上的情况分割和所有目标的简化。第一个子目标自动取消，剩下：1. ！！一份名单[|if a = x then True else x ∈ list; xs = a #list;是的length ys< Suc（length list）→x∈ ys→ x∈ sort ys;26洛杉矶Dennis/Electronic Notes in Theoretical Computer Science 174（2007）if a = x then True else x ∈ list|]=x∈insert a（sort list）突出显示的规则：•“插入x [] =[]”•“insert x（h#t）=（if x≤h then x#h#t else h#insert x t）”•“sort [] =[]”•sort（x#xs）= insert x（sort xs）然后，它通过（排序列表）上的案例进行，然后进行简化，给出两个子目标及其相关的程序切片：1. [|<$x ∈ list; if a = x then True else x ∈ list;sort list =[];if a = x then True else x ∈ list|]=False•“插入x [] =[]”•“insert x（h#t）=（if x≤h then x#h#t else h#insert x t）”•“sort [] =[]”•sort（x#xs）= insert x（sort xs）2. [|if a = x then True else x ∈ list; sort list/=[];x∈list→x∈sort list;if a = x then True else x ∈ list|]=x∈insert a（sort list）• “插入x [] =[]”•“insert x（h#t）=（if x≤h then x#h#t else h#insert x t）”•“sort [] =[]”•sort（x#xs）= insert x（sort xs）这会识别出一个程序片，它参与了产生False目标（[insert_nil，sort_cons]），因此有助于寻找错误。在一些类似的证明中，步骤的情况会自动被排除，在这种情况下，good（sortcons）= bad（sort cons）= 1，规则的注释变成“sort（x#xs）=insertx（sortxs）”作为第一个目标，只留下insert_nil高亮显示为“可能不正确”，从而提供了关于罪魁祸首的进一步线索。在这个特殊的证明中，试图证明第二个目标会导致进一步的证明分支，这些分支会导致归因于insert_nil的错误结论，但也有几个分支被释放这表明用户可能需要访问关于规则的好整数和坏整数的进一步信息。尽管还不清楚如何单独通过语法突出显示来传达这样的信息，但肯定有可能为“最差”规则引入进一步的突出显示(see§5）和/或允许可选地显示好值和坏值，规则，在这种情况下，insert_nil将在本例中被挑出来。洛杉矶Dennis/Electronic Notes in Theoretical Computer Science 174（2007）274.3被卡住假设insert_nil已经被固定，我们将考虑的最后一个例子在稍后的阶段进行主要的验证。我们现在假设插入和排序已经从可疑列表中删除引入了两个新的函数和一个新的引理minl返回一个自然数列表的最小元素，-minl返回一个删除了一个最小元素的列表。除其他事项外，以下引理已经建立：l= []= （ sort l ） = （ minl l ） #sort（−minl l），当用于证明时会导致目标1. count_list x（Once（minl（a#list）#sort（-minl（a#list）= 0突出显示的规则：•“一次[] =[]”•“一次（x1#x2#xs）=（如果x1=x2则一次（x2#xs）else x1#x2#Once xs）”通过案例证明是否−minl（a#list））= []简化第一个目标后留下两个子目标，其中第一个：1. [|a/= x&<$x ∈list;(if a = minl（a # list）then listint [];xs = a # list|]=最小计数_列表x（一次[最小值（a # list）]）= 0与以下高亮显示的切片相关联：•“一次[] =[]”•“一次（x1#x2#xs）=（如果x1=x2则一次（x2#xs）else x1#x2#Once xs）”虽然这5支持性结果这里提出的接口设计背后的想法来自于在证明规划框架内自动检测和修复此类错误的工作[4]。在λClam[13]证明规划系统中实现了程序切片跟踪。在没有实现定理证明接口，我们报告了一些结果，在这个系统内的成功的prostistics我们使用了[4]4中报告的系统的变体。该系统试图修复错误的重写规则。这里报告的系统简单地终止了错误分支，并通过对每个规则r报告好（r）和坏（r）来结束证明尝试。不幸4 相关代码可向作者索取。28洛杉矶Dennis/Electronic Notes in Theoretical Computer Science 174（2007）一些错误，特别是那些出现在递归情况下的定义导致系统是非终止的，因此，如果归纳证明的步骤情况不能通过诉诸归纳假设5来解决，则使用额外的启发式来关闭分支。我们做了两个实验。在实验1中，闭合步骤案例分支对好/坏分数没有贡献（即，严格采用本文提出的惯例）。在实验2中，这种封闭的分支增加了坏分数（可以说，在人类的证明尝试中，这些分支最终会导致一个错误的目标，而不是λClam中导致的非终止）。表2显示了两组运行的结果实验涉及24个非定理，这些定理基于本文中已经涉及的列表追加、列表成员以及插入和排序程序的定义中的错误这些定理是从λClam基准集中选择的，而不是这些函数的实际规范。因此，这些结果仅应被视为指示性的。 对于每个实验，表格报告了“不正确”的重写规则是否被下划线（即，它的好分数是否大于它的坏分数）和加下划线的规则的平均数量。这是当至少有一个规则被加下划线时的平均数-在某些情况下，没有规则的坏整数比好整数大。给出这个平均值的目的是提供证据，证明在多大程度上，这些规则有助于将注意力集中在错误的规则上将没有下划线的规则包括在内，会降低这一平均值，并往往表明比实际情况更好的歧视。为了跟进这一点，我们提供了排除的规则的百分比。这是在证明中实际使用的定义所涉及的规则中没有下划线的规则的百分比。同样，这仅指至少突出显示一项规则以使人产生选择范围缩小的印象的情况。误报报告某些规则被突出显示但不正确的规则未被我们还计算了每个重写规则的得分作为坏得分和好得分的元组。然后根据>where对这些元组进行排序（b1，g1）>（b2，g2）（b1 g2））<和>是自然数的标准顺序。我们报告的百分比的情况下，预期的错误被挑出来的启发式，当它是唯一的规则与最高分。结果表明，如果接口还可以标记那些在>下得分最高的规则，即使所有规则都被用于好分支而不是坏分支，这将是有用的，因为这清楚地给出了关于错误的位置对“卡住”的目标使用糟糕的评分（实验2）是有问题的-它提高了识别不正确规则的比率，以及以失去区分为代价的糟糕规则被突出显示为“最差”的比率（见排除的规则）。由于卡住启发式是一种模仿人类“获得”的粗糙尝试5，除了少数特殊情况，例如，步骤情况证明已经分支如下案件分割洛杉矶Dennis/Electronic Notes in Theoretical Computer Science 174（2007）29实验1.实验2.不正确的重写下划线百分之五十百分之六十六划线规则平均数1.622.11排除的规则百分之五十二百分之三十八假阳性01不正确的重写得分最高百分之六十二点五79.17%不正确的重写具有唯一的最高分数百分之二十九点一七54.17%表2λClam实验结果总结卡”的行为，这也许并不奇怪的结果是模棱两可的。无论如何，很明显，在某种程度上，这种启发式过于急切，并阻止（在第一种情况下）证明进展到错误的分支，如果由人类证明者继续下去，（希望）以后会得到评分，在第二种情况下，产生太多的误报。改进启发式是远远超出了本文的范围，但上述结果的解释需要牢记其局限性。启发式确实表明，允许人类证明者干预评分过程并将某些分支标记为显然，这些结果只是表明了与自动化系统相比，自动化系统如何为人类用户服务，但它们确实表明，可以利用附加在证明分支上的程序切片中包含的信息。特别是6相关工作HAT工具[2]使用算法调试和程序切片的混合，将用户的注意力引导到程序源代码的相关部分。HAT创建了一个求值依赖关系树（EDT），它跟踪样本输入上函数调用的执行序列这个树中的节点可以与它们在程序中的“调用位置”相关联。这允许系统使用语法突出显示机制将调试跟踪与代码的特定部分相关联。该工具的工作原理是识别EDT中的切片，并将这些切片与代码的相关部分关联起来。这最近被扩展[3]为使用与上述非常相似的轮询系统，基于叠加“正确”EDT和“不正确”EDT来生成启发式分数，通过该分数一般来说，HAT工具只显示最直接的redex，而不是一个切片中涉及的所有redex，以减少信息过载-30洛杉矶Dennis/Electronic Notes in Theoretical Computer Science 174（2007）这是我7进一步工作7.1执行显然，最紧迫和最重要的进一步工作是提供基于验证的程序切片的实现，以允许对它真正帮助定位错误的程度进行实验我们的目的是提供一个实现在Isabelle/Isar使用证明一般接口。这允许接口使用的信息和基础定理证明器使用的信息之间有一个清晰的分离。然而，这种方法也带来了一些挑战，因为必须推断目标和证明状态的必要属性总的来说，识别目标和目标中的关键常量应该是相对简单的，尽管在跟踪证明状态方面会有一些挑战，特别是正确更新所需的父目标和子目标之间的关系。在Isabelle中，成功完成的目标从提交给界面的证明状态中删除，这可能会再次在信息跟踪方面提出一些挑战。尽管这里没有展示直接将规则与策略一起使用的示例（例如，Isar中的规则方法），但这也需要触发跟踪信息的更新。一般来说，基于对战术调用的简单分析，这应该是相对简单的。简化是主要步骤，系统使用的确切规则有效地对用户隐藏。 它也是最重要的策略，可以跨多个目标使用，释放一些而不是其他的（因此导致关于成功证明分支的模糊性），并且可以在自己的应用程序中生成和释放用户不可见的新分支。幸运的是，Isabelle还可以使用（上定理的）证明对象来跟踪程序片信息6。我们还没有考虑回溯应该如何与程序切片交互目前的设计假设证明状态是按顺序生成的，并隐含地假设它们只能按顺序回溯。然而，许多定理证明器允许回溯任何开放目标，而不仅仅是最近导出的目标。在这种情况下，接口可能需要存储关于目标与其父级之间的关系的附加信息，从证明状态到证明状态。这个问题也可能意味着最终将程序片信息存储在证明器的证明状态中比存储6 感谢一位匿名推荐人的建议。洛杉矶Dennis/Electronic Notes in Theoretical Computer Science 174（2007）317.2更详细的节目片段到目前为止，我们已经考虑了程序切片，其节点可以用函数定义的简单case结构来识别，但是如果使用更复杂的切片，其中函数调用/子表达式被视为节点（这在将程序切片应用于函数程序时很常见在下面的例子中，同样是真实的，一个学生被要求提供一个函数removeAll，它从第二个参数中删除第一个参数的所有出现。他们似乎是通过类比以前的函数removeOne来编程的，在removeOne中，只有一个事件被删除，并且忘记了替换对此程序的一个调用代码在Isabelle中表示为：普里姆雷克removeAll_nil：“removeAll x [] = []”removeAll_cons：“removeAll x（h#t）=（if x = hthen removeAll x t else h#removeOne x t）”试着证明<$x∈removeAll x l证明通过对l的归纳进行，然后对所有目标进行简化，自动排出基本情况并留下步骤情况目标：1. ！！阿湖<$x∈ removeAll x l=<$（x = a→<$a∈removeAll a l）&（x a→ a/= x<$ x∈ removeOne x l）突出的规则。•“removeAll x [] =[]”•“removeAll x（h#t）=（if x = h then removeAll x telse h#removeOne x t）”使用一些引入规则（impI和conjI）和更多的简化给出了三个子目标，这些子目标基于x是否= h的情况分割，然后（遵循关于∈的引理）h#removeOne x t的头部和尾部的值。其中第一个（其中x = h）自动排出，留下两个子目标，其中第一个是1. [|x/= a;<$x∈removeAll x l|]= 1000/= 1000理想情况下，我们希望强调与此目标相关的规则如下：•“removeAll x [] =[]”•“removeAll x（h#t）=（if x = hthen removeAll x telse h#removeOne x t）”这表明removeAll x t可能是正确的，并且这个目标是基于h#removeOne x t中h的值。这个目标很容易实现，只剩下目标：2. [|x/=a;<$x∈removeAllxl|]=< $x∈removeOnexl再次理想地，我们想要突出显示第二程序切片dif的部分32洛杉矶Dennis/Electronic Notes in Theoretical Computer Science 174（2007）正式地：•“removeAll x [] =[]”•“removeAll x（h#t）=（if x = hthen removeAll x telse h#removeOne x t）”把注意力集中在规则中有问题的部分，这最终会导致错误的目标。在系统中表示这些切片应该足够容易，例如，可以使用一个简单的整数列表来指示规则中的子表达式的位置以及存储在供使用的程序切片中的可疑规则的所有子表达式然而，要想在没有Proof General等接口的帮助下推断出哪个切片与目标相关的信息要困难得多。事实上，为了提供必要的信息，定理证明器7.3势在必行的计划显然，一个长期目标是将这项工作扩展到必要的项目。在这些情况下，我们失去了程序位置和重写规则之间的对应关系。因此，我们需要调整“在证明分支中使用”的概念8结论本文讨论了验证作为程序切片工具的使用。它讨论了如何证明分支可以用来建立程序片的基础上方程重写规则，并描述了一个简单的机制，推导出一个启发式得分的可能性，一个给定的规则是正确的。然后讨论了如何向用户提供所提出的机制依赖于用户识别“可疑”规则。在案例研究中，这些都与程序函数的情况有关，然而，原则上，没有理由不能以相同的方式处理理论中的任何定义或定理，允许以相同的方式处理一般（基于非验证的）证明中的可疑规范和定义一般机制几乎可以肯定地用于任何寻找证明失败原因的情况还需要开展大量的进一步工作，包括执行工作引用[1] D. 阿 斯 皮 纳 尔 Proof general ： 一 种 用 于 开 发 证 明 的 通 用 工 具 。 在 Tools and Algorithms for theConstruction and Analysis of Systems中，Proc TACAS 2000，LNCS第1785卷。斯普林格，2000年。[2] O.奇蒂尔基于源的跟踪勘探。In C. Grelck，F. Huch，G. J. Michaelson和P. Trinder，编辑，函数式语言的实现和应用，第16届国际研讨会，IFL 2004，LNCS 3474，第126-141页Springer，2005年3月。洛杉矶Dennis/Electronic Notes in Theoretical Computer Science 174（2007）33[3] T. Davie和O. 奇蒂尔一个对的就是一个错的。In H. Nilsson和M. van Eekelen，编辑，第七届函数式编程趋势研讨会，第27[4] L. A.丹尼斯用于错误定位和修复的程序切片和中间推理。In W. 阿伦特，P. Baumgartner和H. de Nivelle，editors，IJCAR 2006 Workshop onDisproving -Non-Theorms，Non-Validity，Non-Provability，2006.出现。[5] L. A.丹尼斯使用程序切片和中间推理来识别和修复程序错误。技术报告，诺丁汉大学，2006年。提交给IJCAR-2006年反驳研讨会-非定理，非有效性，不可证明性。[6] L. A. 丹尼斯河Monroy和P.诺盖拉面向证明的调试和修复。In H.尼尔森和M. van Eekelen，编辑，第七届函数式编程趋势，第131[7] L. A.丹尼斯和P.诺盖拉。 从非定理的失败证明中可以学到什么？ 在j. 赫德，E. Smith和A. Darbari，editors，TPHOLs 2005：Emerging Trends Proceedings，pages 45-58，2005.技术报告PRG-RP-05-2，牛津大学计算机实验室。[8] L. Dixon和J.D. 弗勒里奥IsaPlanner：Isabelle中的原型证明规划器In F.巴德，编辑，CADE 19，LNCS第2741卷，第279Springer，2003年。[9] P. Fritzson，N. Shahmehri，M. Kamkar和T.吉莫西广义算法调试与测试。ACM Lett.程序. Lang.系统，1（4）：303[10] R. Harper. 面向证明的调试。Journal of Functional Programming，9（4）：471[11] H. Nilsson和P.弗里茨森懒惰函数式语言的程序调试Journal of Functional Programming，4（3）：337[12] T.尼普科湖C. Paulson和M.温泽尔Isabelle/HOL：A Proof Assistant for Higher-Order Logic，LNCS第2283卷。施普林格，2002年。[13] J. D. C.理查森，A.斯梅尔和我共享的系统描述：使用Arnda-Clam在高阶逻辑中进行证明规划。In C.Kirchner 和 H. Kirchner ， editors ， 15th International Conference on Automated Deduction ，Volume 1421 ofLNCS，pages 129-133. Springer，1998年。[14] N.罗德里格斯和L.巴博萨通过计算对函数式程序进行切片。在Dagstuhl研讨会上超越程序切片，2005年。[15] E. Y.夏皮罗电子邮件 *麻省理工学院出版社，1983年。[16] F. Tip. 程序切片技术综述。 编程语言杂志，3：121[17] M. D. 威瑟程序切片。IEEE软件工程学报，10（4）：352[18] M.温泽尔 对可读的正式证明文件的一般解释方法。 耶氏酵母中贝尔托，G. Dowek，A.赫斯科维茨角Paulin和L.Thery，编辑，高阶逻辑中的定理证明Springer，1999年。