认证计算：构建可靠性证明与计算相结合的新方法

理论计算机科学电子笔记113（2005）45-63www.elsevier.com/locate/entcs演绎证明马丁·里纳德2计算机科学与人工智能实验室，麻省理工学院，剑桥，美国摘要本文介绍了一个认证计算的概念，一个算法不仅产生对于给定的输入x的结果r，但也证明了r是x的正确结果。 这可以极大地提高结果的可信度：如果我们信任在证明，那么我们可以保证r是正确的。通常，在一个有证计算中使用的推理比计算本身要简单得多。 我们提出并分析了两个例子的认证算法。我们开发了指称证明语言（DPL）作为认证计算的统一平台。DPL无缝地集成了计算和演绎，提供了更强的可靠性保证，并为构造证明和证明搜索方法提供了通用的机制。我们已经使用DPL实现了许多著名的算法作为证书，从排序算法到编译器优化，Hindley-MilnerW算法，Prolog引擎等等。关键词：验证，认证算法，程序正确性，证明，证书，雅典娜，DPL1介绍软件系统的完全演绎验证可能非常繁重。从机械上证明一个复杂的软件对于任何给定的输入总是能产生正确的输出是一个重大的挑战。困难部分是由于演绎技术尚未达到相当先进的技术水平，部分是由于软件固有的高度复杂性。然而，形式证明是提高可靠性的极好方法，即使在证明一个系统完全正确是不切实际的时候，我们也想找到它们的用处。1电子邮件地址：arkoudas@lcs.mit.edu2电子邮件地址：rinard@lcs.mit.edu1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.01.03546K. Arkoudas，M.Rinard/Electronic Notes in Theoretical Computer Science 113（2005）45本文提出了一种完全静态验证的替代方案，即部分动态认证。我们不是静态地证明一个算法对所有输入都产生正确的结果，而是将该算法表示为一个证明搜索过程，该过程接受一个输入x，不仅产生一个结果r，而且还证明r是x的正确结果。这种证明算法可以被视为传统算法的工具化版本，经过修改以证明其结果具有演绎推理。推理在运行时执行，并且仅适用于特定的输入x和结果r。完成的证明可以被视为结果r的证明;一旦这个证明被验证，我们可以说r已经被验证的功能不如静态验证强大。它保证不多也不少：如果算法产生结果，该结果是正确的-模逻辑指定什么是正确的。这仍然非常有用，因为它可以防止程序默默地生成一个看似合理但不正确的结果。运行时认证的优点是，它通常比静态验证更例如，考虑一下我们在第4节中给出的统一化例子。Paulson [28]给出了一个统一算法的完整验证，他指出证明“依赖于一个实质性的替换理论，由23个命题和花冠组成......这个项目已经发展得太大，无法在一篇论文中描述...证明并不完全是美丽的。一系列令人惊讶的问题出现了。”最近，使用Boyer-Moore定理证明器对Martelli-Montanari风格的统一算法的正确性证明长达数千行[31]。相比之下，我们的Martelli-Montanari统一过程表示为认证算法，在不到一页的Athena代码中实现[3]这种戏剧性的差异是主要交易的恰当说明：静态验证让我们对所有输入都放心，但很难;运行时认证给我们提供了更有限的保证，只涉及特定的输入和输出，但更可行。另一个重要的区别是，静态证明（如前面提到的Paulson）通常验证软件组件的抽象模型，而不是实际代码;而在认证计算中，定理指的是实时获得的实际结果我们设想运行时认证作为一种方法，应用于软件系统的选定部分，而不是每个部分。在某些情况下，用数学严谨性来描述输出正确性可能是不可行的。对于其他组件，如反应式系统，重要的问题不是输出正确性，而是行为安全性，在这种情况下，其他方法和形式化，如运行时监控[8]或I/O自动机[18]将被应用。3Athena是我们在所有实现中使用的DPL;我们在第3节中描述它。K. Arkoudas，M.Rinard/Electronic Notes in Theoretical Computer Science 113（2005）4547适当的即使正确性有精确的描述并且很重要，认证也可能不被认为是必要的。例如，编译器编写者不太可能对词法分析器或语法分析器进行认证。这些部分被高度可靠的工具很好地理解和自动化，因此认证它们所需的时间将超过收益。然而，我们可能仍然希望验证编译器后端的优化部分2例考虑欧几里得该算法可以用伪代码表示如下：euclid（a，b）=如果b为0，则返回a。否则，返回递归调用euclid（b，amodb）的结果(We将a除以b所得的余数写成amodb。）该算法的正确性取决于数论的以下两个结果：（一）（二）阿克斯|gcd（x，0）= xx，y |y> 0 gcd（x，y）= gcd（y，x mody）如上所述，该算法默认地依赖于这两个定理。为了证明算法是正确的，必须使连接显式化。为了静态验证的目的，我们可以使用b上的强归纳法来证明，对于任何给定的a和b，欧几里得（a，b）产生gcd（a，b）。在我们的方法中，我们将欧几里得方法表示因此，derive-gcd的输出是形式为gcd（a，b）=r的定理。该定理是从公理和严格建立的结果（在这种情况下，等式（1）和（2））使用标准推理方法导出的，例如，普遍专门化、肯定前件、案例推理等。具体来说，我们将derive-gcd公式化如下：derive-gcd（a，b）=如果b为0，则从（1）推断gcd（a，b）=a。否则，令m=a modb（i）。 递归地将derive-gcd应用于b和m以获得形式为gcd（b，m）=r（ii）的定理。由（2），（i）和假设b>0，我们得出gcd（a，b）=gcd（b，m）（iii）。最后，从（iii），（ii）和等式的传递性，我们得到gcd（a，b）=r。我们可以把derive-gcd看作是证明某个结果正确的一种方法--一种“证明算法”。这是一个配方，说明如何获得两个整数的gcd，以及如何说服怀疑的观察者，结果确实是正确的。4[4]值得注意的是，欧几里德自己把他的过程表述为证明算法。 我们引用《几何原本》第七卷命题II的开头：“必须找到AB和CD的最大公测度。如果CD测量AB，因为它也测量自身，48K. Arkoudas，M.Rinard/Electronic Notes in Theoretical Computer Science 113（2005）45重要的一点是我们信任的基础减少。为了相信derive-gcd产生的定理，我们需要相信什么？我们需要相信在证明过程中使用的前提，即命题（1）、（2）和等式的传递性;我们还需要相信我们可以用来计算乘法器和进行数值比较的原始算术运算是正确实现的。假定（1）和（2）以前是从更基本的公理和定义中推导出来的;等式的传递性可以被看作是一个公理;初等算术运算的正确性可以合理地被善意地接受。但是，derive-gcd的控制结构不需要被信任，或为了得到的定理是可信的，这是一个证明算法，如derive-gcd和传统的算法，如欧几里德之间的关键区别。例如，如果derive-gcd执行的条件分析或它对自身的递归调用是错误的，在某种意义上说，它们不能产生正确的结果，那么证明将不会通过，定理将不会成立。但是，如果一个定理是推导出来的，那么它就可以被信任，即使它的推导碰巧是一个伪命题。因此，认证算法强制逻辑和控制之间严格分离，将后者推到可信基础之外。如果我们实现证明算法的语言能够为每个输出theo-rem发出一个证书，这一点就变得更加明显，即，对结果正确性的形式证明。证书可以自动以Athena等语言获得（见下文）。在Athena中，用户可以将derive-gcd应用于两个整数，比如12和8，并得到两个东西，定理gcd（12， 8）= 4和证明该定理的证书。在这种情况下，证书将是一个直线证明，如以下：a. gcd（4，0）=4from（1）b. 4> 0基元c. 8 mod 4= 0基元d. gcd（8，4）=gcd（4，0），来自（2），b和ce. gcd（8，4）= 4 from d，a，and equality transitivityf. 8> 0基元g. 12 mod 8= 4 primitiveh. gcd（12，8）=gcd（8，4）由（2），g和fj.gcd（12，8）= 4从h，e和等式传递性注意，这个证明本质上是derive-gcd应用于12和8的求值迹。还要注意的是，derive-gcd和euclid的渐近复杂度是相同的。形式定理的证明则CD是CD和AB的共同度量。显然，它也是最大的，因为不超过裁谈会措施裁谈会。但是，如果CD不测量AB，那么......” 演讲继续以同样的风格进行。K. Arkoudas，M.Rinard/Electronic Notes in Theoretical Computer Science 113（2005）4549gcd（a，b）=r将具有O（log2 min{a，b}）步。3指称证明语言证明计算可以被看作是一种独立于语言的范式--一种用证明来支持计算的一般风格然而，在使这种方法在实践中可行的过程中，我们面临着一个语言问题：我们需要这样的语言，在这种语言中，像derive-gcd这样的公正算法可以被正确地表达。为了适合于认证计算，编程语言必须在现代语言的标准设施之上提供几个功能。语言必须有一个内置的严格的陈述和证明的概念，而且：• 必须有一个可信的演绎机制，通过它可以推导出公理和定义的结果。• 为了自动完成繁琐的证明步骤，必须有一个完善的证明抽象机制.非常复杂的证明搜索算法（例如，语义表或Knuth-Benzmann完成）必须以可信的方式表示。• 必须有内在的支持自然演绎实践中常见的数学推理。例如，假设和特征变量流量应该自动处理。• 如果需要，产生定理的计算必须能够输出证明，然后可以独立检查。我们对认证编程的主要贡献之一是设计了DPL（命名证明语言）[1]。特别是，我们已经实现了Athena，这是一个多态多排序一阶逻辑的DPL，满足上述所有标准。Athena有两个主要的创新，一个是同义词，另一个是语义。在语法方面，Athena以新颖的方式形式化了假设范围和特征变量范围等关键概念（最值得注意的是，没有像Curry-Howard系统[ 14 ]中那样将它们减少到类型λ演算中的变量范围），这使得引入了语法形式，如假设，pick-any和pick-witness，这些形式紧密地捕捉最常见和最有用的数学推理习惯用法。塞-在精神上，DPL的主要贡献是假设基的概念假设基础的引入作为一个基本的语义抽象，与词汇环境，存储和延续一样，允许对证明理论进行优雅的处理，甚至对于那些难以以非图形方式形式化的逻辑，如Fitch风格的自然演绎，以及证明检查与计算的平滑集成50K. Arkoudas，M.Rinard/Electronic Notes in Theoretical Computer Science 113（2005）45作为一种编程语言，Athena是Scheme和ML传统中的高阶严格函数式语言。这种语言对于认证计算来说具有明显的优势，例如，高阶证明的延续可以自由地传递，这常常很方便。然而，这不是必要的。其他编程语言，例如，诸如Java之类的面向对象的语言，也可以以保守的方式与DPL证明的抽象语法和语义相结合（即，因此，不包含任何DPL证明的Java程序的外观和行为完全符合Java规范的规定）。在演绎方面，雅典娜有一个小的但逻辑上完整的非常简单的推理规则集合，即逻辑连接词和数量词的引入和这将导致最小的信任基础。更复杂的规则可以实现为方法，其可靠性由语言的形式语义保证。自动定理证明器（例如，因此，决议的基础上）可以得到妥善执行。或者，一个强大的现成的ATP，如Vampire [32]可以被用作一个预言机，然后Vampire输出的证明可以使用系统的原始推理规则转换成一个本地演绎这种外包比“自己滚动”的证明器更可取，因为它利用了ATP社区在过去十年中取得的巨大进步。无论哪种方式，拥有这样一个证明器是很重要的，以便在写下证明或证明算法时能够跳过繁琐的步骤。 雅典娜目前使用一种组合 外包（通过吸血鬼）和本地编写的重写方法和其他类型的证明自动化。最后，逻辑框架的一个重要问题是总体“可信基础”的大小。在一个极端，我们可以在一个基本理论中提供公理和原始推理规则的最小初始集合，该理论原则上适用于所有数学，例如ZF，并且只有两种扩展系统的方法：通过保守定义和通过使用所提供的推理规则进行演绎。通过这种方式，一切都与最初的公理和推理规则联系在一起，这些公理和推理规则显然是合理的，因此合理性得到了保障。在另一个极端，允许用户引入任意的公理、推理规则和决策过程，而不需要一个小的初始基础作为锚。第一种方法在原则上是优越的，因为最小的可信基础可以最大限度地提高演绎提供的保证，但在实践中它是不必要的严格。雅典娜采取了中间立场：提供了一个最小的可信基础，用户可以选择只通过保守的定义和演绎来扩展它，从而将所有内容都绑定到该基础上;但这不是必需的K. Arkoudas，M.Rinard/Electronic Notes in Theoretical Computer Science 113（2005）4551≈这样做.他们也可以选择引入任意的公理、规则和决策程序。在哪里锚定证明的选择是留给用户的，由每个应用程序的上下文来决定。例如，在下一节的统一示例中，我们引入五个推理规则作为原语。它们并不是最简单的规则：在最坏的情况下，应用其中四个规则所需的时间与其输入的大小成线性关系，而应用五个规则所需的时间则是二次关系。规则可以进一步简化，用更简单的规则和公理表示为可信方法，尽管代价是额外的工作。但是，即使我们让它们保持原样，我们也已经完成了一个显著的信任减少：我们不必信任传统的Martelli-Montanari算法，它具有复杂的控制结构和指数复杂度，我们只需要信任五个非常短和简单的推理规则，最坏的情况是二次复杂4通过认证算法实现作为一个更复杂的例子，在本节中，我们将使用证明计算来实现一阶统一。传统的归一化算法将两个项s和t作为输入，并为它们产生一个幂等最一般的归一化器（“mgu”）θ，如果存在的话相比之下，我们的统一化证明器将s和t作为输入，不会简单地产生θ，但实际上会证明θ是s的幂等元，t. 换句话说，我们的证明器的输出将是以下形式的定理：imgu（s，t，θ），断言θ是s和t的幂等mgu。第一步是制定一个健全的逻辑，使我们能够得出这种形式的判断。然后，基于这个逻辑，我们可以开始实现一个统一过程作为一个认证算法。在下文中，通过“项”，我们将意味着一些函数符号和变量上的一阶Herbrand项;通过“方程”，我们将意味着一对有序的项s，t，它将更简洁地写为s t ;通过“替换”，我们将意味着从变量到项的函数，它几乎处处是恒等式[2]的文件。我们使用字母x、y和z作为典型变量;f、g和h作为函数符号;s和t表示项;θ、σ和τ表示替换。我们写{x1> →t1，.，xn <$→t n}，用于将每个xi映射到t i的替换（我们假设e，x1，.，xn是不同的）和每一个其他的变量本身;我们写θ为唯一的同态扩张的替代θ到相应的术语代数[34，2]。Martelli-Montanari（简称MM）统一算法[19]处理有限方程组而不是单个方程。由系统52K. Arkoudas，M.Rinard/Electronic Notes in Theoretical Computer Science 113（2005）45联系我们{›→ ›→}···⇒联系我们联系我们我们将意味着一个列表的形式(3)E=[s1] t1，... ，s nn n]。我们把E1和E2连接起来得到的列表记为E1，E2.为了方便起见，我们有时将单个等式视为一个元素列表，例如，写作E，stinst ead ofE， [st]。最后，对于任意θ和形式（3）的系统E，我们记为系统[θ（s1）<$θ（t1），.，θ（s n）<$θ（t n）].一个形式为（3）的系统如果存在一个替换θ使得θ（s i）= θ（t i）（i =1，.），n.我们称θ为E的单位元。如果θ比使E统一的任何σ更一般，那么我们说θ是E的最一般的统一者。大多数一般的单位元直到重命名的复合都是唯一的，在这个意义上，我们可以说某些E的mgu。我们写U（E）为E的所有单位元的集合，其中如果E不是单位元，我们当然可以有U（E）=E。因此，传统的确定两项s和t是否可以统一的统一问题可以简化为确定系统[st]是否可以统一的问题一个系统E被称为解的形式i，其中出现的方程组的形式为{x1<$t1，.，xk∈ k}，其中变量x1，.，x k是不同的，并且对于任何i，j1，.，k. 直接证明了这种形式的系统E确定唯一的代换θ E= x1t1，. ，xktk是E的幂等最一般单位元。MM算法试图通过重复应用以下规则将给定系统转换为求解形式：• 简化：E1，t t，E2E1，E2;• 分解：E1，f（s1，...， sn）f（t1，. ，tn），E2E1，s1t1，.， sn=n，E2;• 转座：E1，t<$x，E2<$E1，x<$t，E2，前提是t不是变量;• 应用：E1，x t，E2x t（E1），x t，x t（E2），条件是x出现在E1，E2，但不是在t。对于任意两个系统E和EJ，我们写E<$EJ来表示EJ可以通过这些规则之一从E换位规则中的限定是保证变换过程的终止所必需的。在最后一条规则中，x必须出现在E1，E2中的限定也是如此（该规则的第二个限定确保过程不会在存在方程x∈t的情况下进行，其中x出现在t中，因为这样的方程是不可统一的）。使用这些变换作为统一两项s和t的算法背后的想法是这样的：我们从系统E1= [s<$t]开始，并不断应用规则（非确定性地），建立一个序列E1<$E2<$Ek，直到我们最终到达一个方程组Ek，其中没有可以应用更多的规则。 证明终止并不困难（即，不可能继续适用无限规则），如果s和tK. Arkoudas，M.Rinard/Electronic Notes in Theoretical Computer Science 113（2005）4553≈[解决形式]►U[x1]t1，.，xn<$tn]：{x1<$→t1，.，xn<$→ tn}假设[x1]t1，.，xn<$tn]是解的形式E1，E2：θ►UE1，tt，E2：θ[回复性]E1，sθt，E2：θ►UE1，t s，E2：θ[对称]UE1，s1 sn≠tn，E2：θ►UE1，f（s1，...，sn）n =f（t1，.，tn），E2：θ[一致性]E1，xθt，E2：θ►UE1′， xθt，E2′：θ证明了{x <$→t}（E1′，E2′）=E1，E2.[抽象]Fig. 1. 一种推导幂等最一般单位元的逻辑。若真的是可解的，则最终系统Ek将处于解的形式，即，它的方程将包括一组形式为Ek={x1≠1，. ，xn≠ n}，其中变量x1，. ，xn是不同的，并且xi不出现在任何t j中。因此，代入θ Ek ={x1<$→ t1，. ，xn <$→ t n}是幂 等的MGU，Ek. 此外，我们可以证明，如果Ei<$Ei+1，则U（Ei）=U（Ei+1），因此，任何使Ei统一的替换也使Ei+1统一，反之亦然。 因此，θ Ek也是E k−1，E k−2，.的幂等元mgu。，E1，因此是s和t的幂等元mgu。另一方面，如果方程的最后一组Ek不是解的形式，那么我们可以得出结论，初始项s和t不可统一。现在我们将建立一个微积分来证明一个方程组是可统一的。 我们可以使用这样的演算来证明两个给定的项s和t可以通过对系统[s t]是可统一的这一结论给出证明来统一。 这样的证明将从断言某些系统显然是可统一的公理开始，并通过应用形式为“如果E1，..的推理规则来进行。“恩，恩。MM变换规则不适合于这个目的，因为它们是从相反的方向进行的：它们从我们希望建立其统一性的方程开始，然后回到其统一性是明显的系统。从这个意义上说，它们是解析的或相比之下，我们想要的是能够让我们向前推进的综合规则：从简单的元素开始事实上，我们将看到，MM算法是，在精确的意义上，一个落后的54K. Arkoudas，M.Rinard/Electronic Notes in Theoretical Computer Science 113（2005）45►{› →}►证明搜索算法的演绎系统，我们制定这里。我们逻辑的判断具有UE：θ的形式，断言替换θ是E的幂等最一般的unier。逻辑本身包括一个公理和四个一元规则，如图1所示。公理[Solved-Form]断言每个方程组E = [x1<$t1，.，xn <$t n]的解是唯一的，θ E={x1<$→t1，.，xn<$→tn}是E. 规则[Rexexivity]、[Symmetry]和[Congruence]是不言自明的，它们的合理性应该是清楚的（可以直接证明所有五个规则都是合理的，而且确实是完整的[1]）。注意，如果我们以向前的方式阅读规则，那么，关于MM变换，自反性可以被看作是简化的逆，对称性可以被看作是换位的逆，而同余可以被看作是分解的逆。我们还将看到[抽象]是应用的逆。还要注意，这些是纯推理规则，在这个意义上，没有控制信息嵌入其中。诸如在MM系统的换位规则中发现的限制将被转移到自动化该逻辑的认证算法的控制结构，从而保持逻辑本身更清晰。最后，讨论抽象规则。 公式o{x→t}（E1J，E2J）=E1，E2在这里. 这意味着E1J，E2j中的方程是一个抽象在E1，E2中的方程，可从后者通过替换某些t的出现x。或者，E1，E2中的方程是E1J，E2j中的方程的实例，通过应用替换，从后者中得到{x<$→t}。因此，E1J，E2J中的方程比E1 j，E2j中的方程更通用，E1，E2让我们用一个例子来说明。我们将证明代入θ=Xa，yg（h（a）），zh（a） 是f（x，g（z），b，z）和f（a，y，b，h（x））的幂等MGU。下面的推论证明了这一点：1.[x<$a，y<$g（h（a）），z<$h（a）]：θ[求解形式]2.[x<$a，y<$g（h（a）），b<$b，z<$h（a）]：θ1，[Re = exivity]3.[x<$a，g（h（a））<$y，b<$b，z<$h（a）]：θ2，[对称性]4.[x<$a，g（z）<$y，b<$b，z<$h（a）]：θ3，[抽象]在z<$h（a）5.[x<$a，g（z）<$y，b<$b，z<$h（x）]：θ4，[Abstraction] onx<$a6.[f（x，g（z），b，z）<$f（a，y，b，h（x））]：θ5，[同余]我们注意到，唯一的规则，即一个判断UE：θ的子项θ，或以任何方式，是公理[解决形式]。所有其他规则都只是简单地传递前提的替换不变。因此，对于一个已解形式的系统，一个替换只产生一次，从那一点开始，它通过各种规则从一个系统带到另一个系统，直到它最终与原始输入相连。我们现在可以实现一个证明算法unify，它接受一个输入系统E，并使用这个逻辑导出一个形式为E：θ的定理，K. Arkoudas，M.Rinard/Electronic Notes in Theoretical Computer Science 113（2005）4555≈≈≈≈假设E是可统一的，否则失败。在下文中，我们将从高层次上勾勒出这样一个算法的轮廓5unify中的大部分工作都是由一个辅助过程find-candidate完成的，它将系统E分成三部分，一个前缀E1，一个方程st，和一个子集E2，以这样的方式，E1，st，E2匹配左手 四个MM规则之一。这三个值在一个三元素列表中返回.如果不存在这样的分解，则find-candidate返回空列表。首先，unify将其输入E传递给find-candidate。如果后者无法像上面讨论的那样拆分E并返回空列表，那么unify检查E是否处于已解形式。如果是，则使用规则[Solved-Form]来证明相应的定理;否则unify失败。另一方面，如果使用某种MM规则T找到某种分解E1，st，E2，则unify使用一个新的输入列表对其自身进行递归调用，该输入列表由E1，s，t和E2适当地构造，然后使用该结果和我们的微积分的相应规则（T的逆）导出关于E的定理。图2描述了当unify应用于系统[f（x，g（z），b，z）f（a，y，b，h（x））]时控制的运行时流程。从本质上讲，每一个原始规则的应用都是对相应递归调用的工作的公正。 当整个证明完成时，我们已经验证了原始问题分解和证明搜索。因此，我们不需要信任候选人或统一，这是迄今为止系统中最复杂的部分。如果我们确信这五个基本推理规则，那么结果是可信的。5相关工作证明计算可以被看作是Rinard和Marinov在MIT [30]和其他研究人员在其他地方[29]关于编译器转换的逻辑验证的工作的概括。在那里，一个优化过程，比如说，常数传播，不仅产生一个转换后的控制流图，但也证明了一个互模拟定理，它与原来的。在这里，我们将这个想法扩展到任意计算。将演绎用于计算目的的想法并不新鲜。它是关系逻辑编程学派的基石[17]，至少可以追溯到20世纪70年代初Prolog的诞生这 种 情况下的计算可以用科瓦尔斯基的著名口号来描述：计算=逻辑+控制。逻辑部分包括我们的理论、公理和推理规则--问题的“是什么”。控制部分相当于5感兴趣的读者可以在www.example.com上找到这个例子和其他例子的实际Athena代码（以及解释性注释）www.cag.lcs.mit.edu/~kostas/dpls/cc-examples。56K. Arkoudas，M.Rinard/Electronic Notes in Theoretical Computer Science 113（2005）45图二. unify的控制箭头（逆时针方向显示）应用于运行的示例;这里的θ是{x<$→a，y<$→g（h（a）），z<$→h（a）}。证明定理的策略--然而，在逻辑编程中，用户不写证明或证明方法;他们只写公理（表示为Horn子句）。控制引擎SLD解析被烘焙到底层框架中，无法扩展。用户不能制定任意的证明策略，为特定的问题领域定制。使用DPL的认证计算非常不同，因为用户在构建控制部分时具有不受限制的自由。除了表达性、通用性和可扩展性之外，逻辑与控制的完全分离也是模块化的好处，因为许多不同的控制引擎可以与单个逻辑一起使用。这便于代码消费者与任意代码生产者的交互。获得可靠软件的另一种方法是静态程序验证，我们已经讨论了它和我们的方法之间的主要权衡，即通用性与可行性。程序验证的另一个优点是静态证明具有固定的成本。一旦建立了正确性，该算法就可以放心地执行任意多次，而无需额外的计算。相比之下，我们的模型有一个运行时的代价：算法必须做额外的工作，以证明自己每次生成一个结果。然而，根据我们的经验，运行时认证从来没有严格地unify[f（x，g（z），b，z）<$f（a，y，b，h（x））]{f（x，g（z），b，z）<$f（a，y，b，h（x））}：θ（分解）（反转）vˆ同余unify[x<$a，g（z）<$y，b<$b，z<$h（x）]（适用）vunify[x<$a，g（z）<$y，b<$b，z<$h（a）]（适用）vunify[x<$a，g（h（a））<$y，b<$b，z<$h（a）]（转置）vunify[x<$a，y<$g（h（a）），b<$b，z<$h（a）]{x<$a，g（z）<$y，b<$b，z<$h（x）}：θ ˆ抽象{x<$a，g（z）<$y，b<$b，z<$h（a）}：θ ˆ抽象{x<$a，g（h（a））<$y，b<$b，z<$h（a）}：θ ˆ对称{x<$a，y<$g（h（a）），b<$b，z<$h（a）}：θvunify[x<$a，y<$g（h（a）），z<$h（a）]ˆ回复性）2019 - 05 -2201： 01：02（（a）），zh（a）已解形式}：θK. Arkoudas，M.Rinard/Electronic Notes in Theoretical Computer Science 113（2005）4557增加了算法的渐近复杂度。软件模型检查[22，35]不太关心为特定输入建立输出正确性，因为它是在尽可能大的输入类上发现错误，重点是并发问题，如死锁，临界区违规等。在软件测试[5]中，大量的输入样本被提交给程序，并检查输出的正确性。虽然测试在实践中仍然是宝贵的，但它有严重的缺点。首先，结构复杂的输入数据的生成很难自动化[15]，因此测试套件最终非常有限。第二，如何检查输出的正确性？肉眼检查显然不适用于大规模实验。因此，必须编写软件来检查输出对于给定的输入是否正确。但是这样的我们稍后会详细说明这一点。最后，测试是一个经验的、有限的过程;它不能测试所有的输入。通常，在程序发布后，它开始为某些输入组合生成错误的结果，而这些输入组合只是在测试过程中被遗漏了为了克服上述最后一个问题，Wasserman和Blum [33]建议将正如作者承认的那样，这只适用于这样的问题，即检验结果的时间比生成结果的时间渐近更短，也就是说，只有当C的复杂性严格小于A的复杂性时，才有意义将算法A与检验器C耦合。他们称之为“简单跳棋”不幸的是，简单的跳棋通常不存在。在许多情况下，检查器C独立确定结果r对于输入x是否正确的最有效方法是重新计算其自己的结果rJ，然后比较r和rJ是否相等。因此，测试程序将与算法本身具有相同的复杂性，我们没有理由相信它比原始算法更重要。在这种情况下的测试相当于“冗余编码”;它是低效的，对提高我们结果的可信度没有什么价值。 例如，考虑排序。 为了检查输出列表LJ对于输入列表L是否正确，检查器首先需要验证LJ是排序的，这相对容易-它可以在长度为LJ的线性时间内完成。但它也需要验证LJ是L的置换最直接的算法需要二次时间，即，它比排序本身更昂贵，排序本身大概花费了nlogn时间。为了以更好的最坏情况性能进行更多的排列检查，检查器将被简化为对L进行排序，得到58K. Arkoudas，M.Rinard/Electronic Notes in Theoretical Computer Science 113（2005）45∩···结果LJJ，然后检查LJJ和LJ是否相等，从而实现零信任降低。这似乎是大多数多项式时间算法的情况：它们的检查器要么和算法本身一样昂贵，要么只是稍微好一点。解决棘手（NP完全）问题的算法确实有非常简单的检查器，能够验证肯定答案。这直接从NP类的定义中得出。例如，考虑一个判定图是否是哈密尔顿图的算法H。我们可以有效地检查然而，我们不能有效地检查H的否定答案。事实上，在NP/ = co-NP的假设下（这是一个广泛持有的信念[25]），很容易证明没有NP完全问题可以在co-NP中，这意味着没有有效的检查器能够验证NP完全问题的否定答案因此，真正简单和完整的检查器似乎只存在于NP co-NP中也被认为位于P之外的问题，例如整数分解。Blum例如，在上面的排序示例中，我们可以检查是否LJ= [y1，.，y m]是L= [x1，. .. +h（xn）和s2=h（y1）+ +h（ym）。 这可以在线性时间内完成，并且如果LJ确实是L，则s1=s2;否则这两个和可能不同。错误的概率可以任意小，但是在运行时需要越来越多的检查来收敛，进一步损害了运行时性能。目前还不清楚这些技术的适用范围有多广;它们似乎更适合于数值问题。因此，与计算机科学中认为检查结果比生成结果更容易的民间智慧相反，检查结果通常与生成结果一样困难。事实上，在某些情况下，这甚至更困难，甚至完全不可能。一个最好的例子出现在编译中：虽然可以--而且相对容易--机械地找到一个机器语言可执行文件，它模拟源语言中的给定程序，但不可能机械地检查给定的机器语言程序是否没有这样的检查器存在，因为问题是不可判定的。作为另一个例子，考虑Prolog查询的执行。如何检查“是/否”查询答案？ 不可能建立一个完整的、正确的检查器，因为问题是不可判定的：一个假的“是”的答案可能会让我们的检查器进入无限循环。但两K. Arkoudas，M.Rinard/Electronic Notes in Theoretical Computer Science 113（2005）4559这些问题和许多其他问题都很容易接受我们的方法。Athena已被用来实现可信的编译，以及一个认证的Prolog系统，备份其答案与非常简单的自然演绎推理。Meyer的契约编程范式[ 20 ]中的可执行断言对于动态执行健全性检查和确保某些简单的前置条件和后置条件成立非常有用简单断言（仅包含内置原语，如算术运算和比较、其布尔组合和有界量化）是可信的，但不能表达许多有用算法的输出正确性。例如，这样的断言不能确定高斯-乔丹消去算法是否正确地确定了给定的线性方程组没有解;符号积分程序是否正确地积分了给定的函数;字符串是否正确地匹配了正则表达式模式;等等。即使这样的断言可以捕获输出正确性，它们也经常以朴素的声明风格这样做，因此它们的运行时执行变得不切实际。例如，有许多问题--例如最短路径图问题--可以通过程序高效地解决，例如，使用动态编程技术，但其声明性输出规范需要指数时间来检查。当然，允许指定断言包含任意可执行代码（例如，Jass [4]中的断言可以包含任意的无副作用的Java代码）。在这种情况下，可以对任意计算执行完整的正确性检查，但检查代码的信任问题会原封不动地重新出现。我们认为诸如面向监视器的编程（“MoP”[ 8 ]）和运行时验证[16，13]等技术对于许多问题，在这样的框架中保证输出正确性是困难的或不可能的，因为我们在前面的段落中讨论过的规范简单性和信任之间的紧张关系。例如，ASML [3]和JML [7]的前置条件和后置条件简单且易于信任，但使用了有界的非确定性选择和量化，因此无法表达感兴趣问题的正确性，或者执行起来过于低效我们可以通过将ASML和JML规范编写为维护变量、更新状态、执行循环等的“模型程序”来解决这个问题，但这样一来，规范就变得过于可操作。6、技术[6]例如，gcd算法的声明性正确性后置条件执行起来非常不准确。或者，我们可以将Euclid的算法表示60K. Arkoudas，M.Rinard/Electronic Notes in Theoretical Computer Science 113（2005）45诸如MoP和运行时跟踪验证对于以经认证的计算不能的方式使用内联和内联监视的组合来观察和操纵系统的动态行为是非常有用的，最显著的是为了确保系统状态的安全属性、检测协议违反并对协议违反做出反应、引发适当类型的异常等。因此，我们设想将这些技术与认证计算结合使用，以确保软件组件实现符合其规范的不同方面。Lee和Necula [23]的证明携带代码（PCC）主要是一种编译方法，涉及生成满足某些安全策略的程序，因此可以“安全”执行。这需要一般的验证，因为程序必须被证明对所有可能的痕迹都是安全的。这有多困难取决于所涉及的特定安全概念。相比之下，认证计算是一种通用的计算范式，关注于确保特定输入输出对的正确性，而不是所有输入的安全当然，输出内存或类型安全证明的在演绎技术的问题上，我们注意到一个证明算法原则上可以在任何语言中实现，例如在C语言中，只要它最终产生一个形式证明（比如LF [12]或Coq [9]或Athena形式），然后可以独立检查。但这将混淆用于文件目的的扣除，也将是不适当的阻碍-一些。算法认证与证明工程有着千丝万缕的联系，因此，通过为构建和管理形式理论、执行证明搜索以及构造和验证形式证明（见第3节）提供规定的系统，算法认证得到了极大的促进。因此，LCF风格[10]系统，如HOL [11]或Isabelle [27]，当然可以用于证明计算。然而，我们的认证算法与米尔纳开创性的“战术”和“战术”无关策略是反向