理论计算机科学电子笔记174（2007）75-86www.elsevier.com/locate/entcs验证工程Anne Mulhern1，2 Charles Fischer3 Ben Liblit4美国威斯康星大学麦迪逊分校计算机科学系摘要现代集成开发环境（IDE）为程序员提供了各种用于程序可视化和操作的复杂工具。这些工具帮助程序员理解遗留代码，并在程序的大部分中进行协调更改。 集成证明环境（IPE）中包含的类似工具将帮助证明开发人员理解和操作正在开发的越来越大的证明。在本文中，我们提出了一些工具和技术开发的软件工程，我们相信将同样适用于证明工程。关键词：IDE，IPE，证明可视化，程序可视化，重构，程序提取，Coq，证明依赖，证明转换，证明策略，证明框架，证明重用，证明解释1引言现代集成开发环境（IDE）为程序员提供了各种用于程序理解和操作的复杂工具。除了语法突出显示和项目构建等基本功能之外，这些工具通常还提供了更好的重构和程序可视化组件。许多为IDE开发的技术可以直接转移到可编程逻辑器件领域。其他的可以被修改以利用定理证明器的特殊性质将IDE技术转移到定理证明器的想法并不新鲜[2，7，21，36]。然而，在过去十年中，IDE取得了重大进展。这些进步中的许多都是由开发人员的需求推动的，他们必须维护和扩展大量现有代码。现实世界的程序越来越复杂，这意味着即使是有经验的程序员也很难理解1这项工作部分得到了女科学研究生露丝·迪基助学金的资助。2 电子邮件地址：mulhern@cs.wisc.edu3电子邮件地址：fischer@cs.wisc.edu4电子邮件地址：liblit@cs.wisc.edu1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.09.02376A. Mulhern等人理论计算机科学电子笔记174（2007）75不同软件组件之间的关系在扩展或修复现有代码时，程序员可能会花费数小时或数天的时间来计算这些更改可能会影响程序的哪些其他部分。此外，程序员必须进行的更改可能分散在几个程序组件中。出于这个原因，已经开发了许多软件管理工具来帮助可视化程序属性。其他允许程序员轻松导航项目，并在多个文件中进行自动更改。随着自动定理证明的成熟，旧证明与新证明的比例以及它们的规模将继续增长。可视化、理解和自动更改这些证明的工具将变得至关重要。集成验证环境（IPE）5应该以与IDE相同的方式整合这些工具在下面的章节中，我们将讨论几种在软件开发中有用的技术，这些技术可以扩展到定理证明。这些技术是通过派生导航，多视图，自动重构和大规模的证明可视化2通过派生形式证明，即使是相对简单的证明，也必然非常庞大。例如，Coq [35]中数独谜题的形式化和伴随的求解过程需要大约5000行。四色定理的正式证明[12，41]花费了大约60，000行和几年的时间。先进的自动化证明助手已经开发出来，以协助建设这样的证明使用战术。这些策略可以由用户手动选择或由证明助理自动选择。由这些策略生成的证明对象的结构对于用户来说可能是难以预测的，即使当用户已经选择了策略时。当自动选择策略时，结构可以是进一步模糊。证明对象本身可能太大而不容易阅读。例如，上面提到的数独发展包含了两个列表上的排列关系可逆的证明 也就是说，如果一对列表是彼此的排列，并且列表的头部元素相等，则两个列表的尾部也必须是彼此的排列。大约需要10行策略来完成定理的证明，但在大约750行时，生成的证明要大两个数量级尽管如此，在许多情况下，有必要研究这种证明。在证明助手中实现的策略 用户可能正在开发一个证明，专门利用证明助手可能有必要重新发现使用什么辅助定理来证明给定定理;这样的辅助定理可以在没有用户5 作者要感谢一位匿名评论者用这个词来解释他们。A. Mulhern等人理论计算机科学电子笔记174（2007）7577Fig. 1.三面板验证导航工具的总体结构。 证明来自Coq List库，Coq发行版中的标准库之一。左右两侧的滚动条允许用户分别导航证明脚本和派生程序。大多数程序员都熟悉Unix的索引工具，它可以识别两个文件之间的文本索引许多可视化工具都利用了底层的可视化工具。例如，EclipseCompare视图允许用户最多比较三个文件。该工具自动对齐文件之间的差异，并使用视觉提示匹配相应的部分。这种使用视觉线索来识别关联实体的技术可以扩展到其他领域。比如说，证明开发者通常对给定的证明具有两个视角。第一个视角包括定义和定理以及相应的第二种观点由相同的定义和定理组成，这次与它们的证明有关。在策略和证明的条件之间有一种对应关系。这种对应关系不同于文件比较中的对应关系。在某种程度上，它更直接，因为证明与策略有形式上的关系，而在文件比较中，文件之间的关系必须通过启发式发现。然而，对应关系也更加复杂。一种策略可能对应于证明中的多个项。 因此，允许用户选择策略或策略组并通过突出显示证明中的相关术语来响应的交互式工具将是对证明理解的有价值的帮助。一些定理证明者，例如，PX [13]，Minlog [22]，Isabelle/HOL [23]，NuPRL[24]和Coq [34]利用Curry-Howard同构[10，40]来实现程序提取工具[19，20，27]。一个程序提取设施自动生成程序的证明。在提取过程中，删除了证明的逻辑部分，并将计算部分转换为78A. Mulhern等人理论计算机科学电子笔记174（2007）75图二.证明列表上相等的可判定性。左侧的“策略”窗格显示证明策略，而右侧的“程序”窗格显示提取的程序。“校样”窗格显示正确的校样。目标语言从其所需属性的证明中提取的程序称为认证程序。只要提取工具和证明检查器本身是正确的，就可以保证一个经过认证的程序是其规范的正确实现，即，它所提取的证据一般来说，提取的在具有提取机制的定理证明器的情况下，三路关联将是适当且有用的。图1显示了这种导航工具的总体结构。每个组件与相邻面板中的相应组件相关联。证明脚本组件的示例是具有策略的定义或定理，证明组件的示例是定义或证明，提取程序中的组件的示例相应的组件会自动对齐，因为用户专注于校对脚本或提取程序中的不同区域。浅灰色用于证明脚本中未包含在证明中的部分，狭窄的灰色条也用于分离证明和程序组件，A. Mulhern等人理论计算机科学电子笔记174（2007）7579图三.证明列表上相等的可判定性。 用户已在列表eq dec函数中突出显示h参数。函数中h参数的使用和证明中相应的H参数都被强调了。nents。淡蓝色表示组件是从证明脚本中的组件间接生成的。在这个例子中，已经自动生成了列表类型的一些归纳原则。证明的某些组件在提取的程序中没有相应的组件在这种情况下，相邻的分隔符在程序窗格中合并图1中的工具可用于高级检查。用户还可能希望更详细地检查各个证明实体。图2显示了一个证明及其相关的策略和程序。在左侧的战术面板中，自动战术已被选中。前面的战术为绿色，后面的战术为黑色。由突出显示的策略生成的证明项本身被突出显示，并且由前面的策略生成的证明项是绿色的。 “校样”窗格左侧的栏汇总了整个校样。请注意，在条形图的底部有一条绿线，表示生成了证明的最后几行80A. Mulhern等人理论计算机科学电子笔记174（2007）75见图4。显示语法突出显示的校样脚本视图。 突出显示方案改编自CoqIDE中的方案。汽车前的战术。右侧的“程序”窗格显示提取的程序。生成的程序中的相应术语将突出显示。在前面的示例中，证明中的元素是通过证明脚本选择的。也可以通过提取的程序选择这些元素，或者通过证明选择程序中的元素。图3显示了与前面相同的证明。然而，在这个例子中，用户在Program窗格中选择了一个元素，特别是h，列表eq dec函数的形式参数。h在列表eq dec中的使用以及证明中相应的元素被突出显示。“校样”窗格中的摘要栏指示除了文本中可见的匹配项之外，没有其他匹配项。这证实了我们对证明的直觉。h是决定两个列表元素是否相等的函数。它的相应证明H是列表元素上等式的可判定性的证明。h应用于每个列表的头元素以确定两者是否相等，并且在元素相等的情况下作为递归调用中的参数传递（否则listeq dec返回false）。在相应的归纳证明中，我们会期望H也只被使用一次，作为证明列表相等的假设，如果它们的头和尾相等，我们看到情况就是这样。当一个程序在调试被启用的情况下编译时，编译器会在生成的对象文件中编码额外的信息供调试器 特别是，它存储调试器的使用这些信息，符号调试器可以执行机器指令，并向用户显示相应的源代码。我们设想一个类似的方法定理证明。当证明器执行策略以生成证明时，它可以存储策略与所生成的证明对象之间的映射，从而使其可用于诸如上述的程序导航工具。我们已经观察到，策略和证明对象之间的对应关系可能很复杂;但是编译器和调试器能够A. Mulhern等人理论计算机科学电子笔记174（2007）7581(a) 折叠的轮廓视图（b）带剖面的轮廓视图列表上的函数已扩展图五、校样脚本大纲的视图生成和导航源代码和高度优化的机器代码之间同样复杂的映射。3常见便利3.1多个视图在IDE中普遍存在的高亮显示，在一些证明助手中以某种形式可用[29，34]。图4显示了一个Coq证明脚本。不同种类的关键字通过使用不同的颜色来区分，这有助于我们理解我们正在查看的程序的一小部分的基本结构。当我们缩小时，语法着色实际上变得毫无用处。但是这个问题可以通过许多IDE中已经使用的技术来解决。例如，Eclipse [9] Java Perspective提供了一个Outline视图，它允许用户可以一目了然地看到单个文件的基本结构Outline视图是也用于导航。图5示出了图4的证明脚本的建议大纲。另一个可以直接扩展到证明助理的想法是折叠和扩展源文件部分的技术。程序员通常希望省略源文件中某些不相关的部分，以便文件的其余部分 以类似的方式，证明开发人员可能希望82A. Mulhern等人理论计算机科学电子笔记174（2007）75见图6。一个证明的可判定性的平等名单与两个功能崩溃。通过允许光标悬停在箭头上来检查折叠的函数;按下箭头将导致函数展开。省略证明脚本、证明或其相关程序的部分。 图6显示了列表上等式的可判定性的证明，其中两个函数被折叠。第一个折叠函数证明了在尾部不相等的假设下，列表头部的相等是不相关的（在这种情况下，很明显列表是不相等的）。第二个函数是一个类似的证明，但正反颠倒。这样的子证明，虽然需要完成一个正式的证明，在某些情况下，构成整个证明的一个重要比例，一般是无趣的人类读者。3.2自动重构重构是一种重组程序的方法，这样程序的整体组织得到了改善，但行为保持不变[25]。如果证明的大部分是单独开发的，重构可能是必要的，以使不同组件的基本假设相同[12]。重构也可以促进证明的重用[16]。 虽然现代IDE对自动重构的支持更广泛[30，37，38]，但对自动重构的支持却很少。IDE不支持函数和变量的重命名，而PHP应该为引理的重命名提供类似的功能。IDE提供了重构程序的工具;例如，局部变量可以转换为Java类定义中的字段在同一A. Mulhern等人理论计算机科学电子笔记174（2007）7583在某种程度上，CUP应该提供更好的工具来重构现有的证明脚本;例如，在Coq中，用户可能希望将一组证明实体封装在一个模块中。在Eclipse Java IDE中，开发人员可以泛化字段的类型，将字段提升到其超类型[38]并适当地更改字段的所有用途类似地，PHP应该更好地支持重构，以抽象定义和假设[28]。许多其他重构可能依赖于个人证明助手的逻辑和组织。此外，我们提出了一个类似于IDE开发人员使用的“最佳e引擎”标准的转换要求。当开发人员更改方法的签名时，IDE可以通过适当地更改所有重写和重写方法的签名来“尽最大努力”。但是，如果签名被添加的形参改变了，通常不可能自动确定在调用站点传递的实际参数。在转换之后，所产生的类型不匹配将在程序中引起编译器错误。但是，IDE通过自动执行程序员原本需要手动执行的任务，减轻了程序员的任务。程序员可以通过识别必须更改的调用位置、确定要在每个调用位置传递的实际参数并正确地更新代码来完成转换。一般来说，编译器本身将帮助程序员识别必须通过特定错误消息更新的调用位置。CROP开发人员可能会觉得，自动转换会使正确的证明变得不正确，这是完全不可接受的。我们认为，如果转换得到的证明开发人员“更接近”正确的证明，他实际上希望这样的“最佳的eHort”的转换仍然是有价值的，值得纳入一个CUP。开发人员可能只有在对某个组件必须更改的证据进行了大量工作之后才意识到这一点。例如，一个列表不仅必须具有列表的熟悉属性，而且还必须具有其元素被排序以完成证明的额外属性。在Coq中表达这个附加属性的一种方法是通过使用依赖类型[3]。如果开发者改变列表的类型以包括它是排序的证明，那么任何以前开发的包含这个列表的定理也必须改变它们的类型。实现这种简单的转换相对容易。重构工具甚至可以修改某些不依赖于sorted属性的证明的策略脚本，以便完全重构证明但是也许开发者现在必须构造额外的引理来证明排序属性被证明中定义的一些变换所保持。如果没有开发人员的额外手动工作，证明就无法完成。尽管如此，一个重构工具，自动化的简单步骤，并留下开发人员执行更困难的步骤，不能很容易地自动化将是可取的。84A. Mulhern等人理论计算机科学电子笔记174（2007）754在大的程序可视化是一个成熟的领域。在教学[5，15]和专业领域[39]中使用了可视化表示程序的技术，并且不断开发新技术[18，26，31，32]。这些技术包括静态可视化[18，5，39，26，32]和动画[15]。它们通常使用复杂的视觉词汇来传达程序中许多实体之间的关系。Ball和Eick [1]的一个重要见解是，一个不太复杂的视觉词汇也可以传达有用的信息。它们展示了如何使用着色方案它们使用颜色来编码单个行的一元属性，例如行被更改的这样的着色可以允许程序员一目了然地看到程序的一些整体属性。例如，系统中以红色为主的部分经常被编辑，并且很可能包含错误。蓝色的部分编辑频率较低，并且可能相对没有bug。这种方法可以扩展到更大粒度的文本单元，如过程或文件，并已用于故障定位等应用程序[17]。证明可视化的技术不太常见。[14]第十四话对于受限域，例如图形属性[11]。静态可视化技术用于描述证明实体之间的关系[4，6]。我们认为，球和Eick的见解可以应用到证明可视化以及程序可视化。它们可以以一种直接的方式被应用于编码诸如修改信息之类的性质，这些性质在证明和程序之间是真正相同的其他属性更具体的是BMPs。在具有自动组件的证明助手中，可以应用定理，而无需用户特别请求它们。一个对不同定理使用的相对频率进行编码的着色方案可以用来可视化5结论我们已经描述了一些方法，在这些方法中，开发用于帮助程序员维护和扩展大型程序的技术可以用于证明必须维护和扩展大型证明的开发人员。许多软件项目涉及相当多的人工作数年。随着自动定理证明的学科逐渐成熟，类似规模和复杂性的证明，现在被认为是非凡的[41]，将变得更加普遍。程序抽取作为一种开发必须正确的程序的技术正在得到人们的认可随着这些趋势的继续，我们所描述的工具将变得越来越有价值。此外，我们认为开发我们所描述的工具的理论困难是可以忽略的。例如，第2节中描述的导航工具需要底层编码，该底层编码记录A. Mulhern等人理论计算机科学电子笔记174（2007）7585证明脚本、其关联的证明和派生程序。很明显，这些数据是可用的。证明脚本中的实体与其对应的证明之间的关系必须由开发证明的证明引擎计算类似地，证明中的项与所提取的程序中的对应项的关系必须由程序提取机制来计算。困难不在于建立这些关系，而在于记录它们并以有用的方式展示它们另一方面，这一领域的工作可能会产生重要的理论见解。3.2节中描述的重构都非常简单，只是比文本替换复杂有些程序重构要雄心勃勃得多。例如，Tip等人[37]描述了从不利用多态类型系统的Java程序到利用多态类型系统的Java程序的重构。对于定理证明器来说，更雄心勃勃的重构很可能会产生意想不到的见解。确认我们要感谢Kenneth Kunen博士的建议和鼓励。引用[1] 球，T。和S.G. Eick，Software visualization in the large，IEEE Computer29（1996），pp.33-43号。[2] Bertot，Y.，CtCoq系统：设计与体系结构，形式化ASP。Comput. 11（1999），pp. 225-243[3] Bertot，Y.和P.Casteran，[4] Bertot，Y.，O. Pons和L.陈文辉，交互式定理证明器的相关图，技术报告RR-4052，INRIA（2000）。[5] BlueJ-Teaching Java-Learning Java，http://www.bluej.org/.[6] Boite，O.，使用扩展归纳类型证明重用，in：K. Slind，A.邦克和G. Gopalakrishnan，编辑，第17届高阶逻辑定理证明国际会议论文集，计算机科学讲义3223（2004），第17页。50比65[7] 卡普兰，J.E.和M. T. Harandi，A logical framework for software proof reuse，SSR106-113[8] 克鲁斯-菲利佩湖和P. Letouzey， A large-scale experiment in executing extracted programs，in：12thSymposiumontheIntegrationofSymbolicComputationandMechanicalReasoning ，Calculemus'2005，2005，待发表。[9] Eclipse.org主页，http://www.eclipse.org/。[10] Girard，J.-是的，P. Taylor和Y.Lafont，[11]格洛，P. A.，D. B.约翰逊，F。张文龙，一个图形算法的，技术报告PCS-TR 92 -180，计算机科学，汉诺威，新罕布什尔州，达特茅斯学院（1992）。[12] Gonthier，G.，四色定理的计算机验证。[13] 林山和H.中野，[14] 林，S.，R. Sumitomo和K. 《易经》云：“以经为经，以经为经，以经为经。Comput. Sci. 272（2002），pp. 177比195[15] Jeliot：：Home，http://www.cs.joensuu.fi/Jeliot/.86A. Mulhern等人理论计算机科学电子笔记174（2007）75[16] John s en，E. B. 和DC。 Lüth，通过为marti on提供数据库来重新使用。，i n：K. Sl i nd，A. BunkerandG. Gopalakrishnan，编辑，第17届高阶逻辑定理论文集，计算机科学讲义3223（2004），第17页。152-167。[17] 琼斯，J.A.，M. J. Harrold和J. Stasko，可视化测试信息以辅助故障定位，在：ICSE467-477.[18] 琼 斯 ， J 。 一 、 A. Orso 和 M.J. Harrold ， Gammatella ： Visualizing Program-Execution Data forDeployed Software，Information Visualization3（2004），pp.173-188。[19] Letouzey ， P. ， 一 种 新 的 辅 酶 提 取 方 法 。 Geuvers 和 F. Wiedijk ， editors ， Types for Proofs andPrograms，Second International Workshop，TYPES 2002，Berg en Dal，The Netherlands，April24-28，2002，Lecture Notes in Computer Science2646（2003）.[20] Letouzey，P.，“P r g r am m at i o n fonct i onne l le ce r t i i'ee- L ' e xt r act i o n d e p r am m e d an s l ' as is t a n t C o q，“P h. D. si s，Univer s it'ePari s-Sud（2004）.[21] 罗志在证明工程中开发重用技术，在：AISB95会议录，自动推理研讨会：弥合理论与实践，She Bleeld，英国，1995.[22] 明洛系统，http://www.minlog-system.de/。[23] Nipkow，T.，L. C. Paulson和M. Wenzel，[24] PRLAutomated Reasoning Project at Cornell，http://www.cs.cornell.edu/Info/Projects/NuPrl/。[25] Opdyke，W. F.、“重构面向对象的框架”，博士论文，Champaign，IL，USA（1992）。[26] PANA S ， T. ， R.林 克 和 W 。 Lüowe ， TheVizzAnalyzerhandbok， Tecchnicalreport ， Vüaxjoüuniversity（2005）.[27] Paulin-Mohring角和B.Werner，Synthesis of ML programs in the system Coq，J.符号Comput.15（1993），pp. 607-640[28] 庞斯，O.， 证明泛化和证明重用。[29] Proof General，http://proofgeneral.inf.ed.ac.uk/.[30] Rajesh，J.和D.Janakiram，Jiad：a tool to inferred design patterns in refactoring，in：Proceedingsof the 6th ACM SIGPLAN international conference on Principles and practice of declarativeprogramming（2004），pp.227-237[31] 罗德里格斯，N.，Haskell切片， http://labdotnet.di.uminho.pt/HaSlicing/HaSlicing.aspx网站。[32] Rodrigues ， N.F. 和 L.S. Barbosa ， Component identification through program slicing ， in ：Proceedings of the Second International Workshop on Formal Aspects of Component Software，2005。[33] Rosenberg，J.B、 美国纽约州纽约市，1996年。[34] Coq开发团队，[35] 你好，L.， Sudokuin Coq（2006）.[36] 你好，L。、Y. 我是T和G。 Kahn，Realt heremp r or o r o rov ersde servereluser-i n terf aces，in：SDE5 ： ProceedingsofthefifthACMSIGSOFTsymposiumonSoftwaredevelopmentenvironments（1992），pp. 120比129[37] T i p，F. 、R. 去吧，J。 Dolby yanddA. Kiezstecun，Refactoringtechni qesformigratingaplicicJavacontainer classes ， IBM Research Report RC 23238 ， IBM T.J. Watson Research Center ， YorktownHeights，NY，USA（2004）。[38] Tip，F. 、杨A. KiezstecunnandD. Büaumer，Refactoringfororgeneral i zato n ungypeconstra i nts，in：Obj ect-Oriented Programming Systems，Languages，and Applications（OOPSLA 2003），Anaheim，CA，USA，2003，pp. 13比26[39] 对象管理组- UML，http://www.uml.org/。[40] Wadler，P.，Proofs Are Programs（2000）[41] Wiedijk，F.， 世界的十七个证明者（2005）
我的内容管理
展开
