动态检测程序不变量集成Daikon和ESC/Java：静态验证方法

网址：http://www.elsevie r. n l/l oc ate/en tcs/vol um e55. ht ml 22页动态检测程序不变量的静态验证：集成Daikon和ESC/Java杰瑞米·W作者声明：Michael D.麻省理工学院计算机科学实验室美国马萨诸塞州剑桥市科技广场200号，邮编：02139电子邮件：fjwnimmer，mernstg@lcs.mit.edu摘要本文介绍了如何集成两种互补的技术来处理程序不变量：动态检测和静态验证。动态检测提出了基于程序执行的可能不变量，但不能保证所得到的静态验证-阳离子检查属性总是为真，但是选择一个目标和注释程序以输入到静态检查器可能是困难和乏味的。结合这些技术克服了各自的弱点：动态检测的不变量可以注释程序或为静态验证提供目标，静态验证可以验证动态工具提出的属性我们已经集成了一个工具，用于动态检测可能的程序不变量，Daikon，静态验证程序属性，ESC/Java的工具。Daikon检查程序变量的运行时间值;它在这些值中寻找模式和关系，并报告在测试运行期间从未被伪造的属性，以及满足某些其他条件的属性，例如统计上的公正性。ESC/Java将带有前置条件、后置条件和其他断言注释的Java程序作为输入，并且它报告哪些注释不能被静态地验证，并且还警告潜在的运行时错误，诸如空解引用和越界数组索引。我们的原型系统运行Daikon，将其输出作为ESC/Java注释插入到代码中，然后运行ESC/Java，报告不可验证的注释。整个过程是完全自动的，尽 管 用户 可 以 提 供 指导 ， 以 便在 需 要 时 改 进结 果 。 在 初 步 实 验 中，ESC/Java验证了Daikon提出的所有或大部分不变量。c2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。21介绍静态和动态分析具有互补的优势和劣势，因此将它们结合起来具有很大的前景。静态分析通过检查程序源代码和对可能执行的推理进行操作。它构建程序状态的模型，例如变量和其他表达式的值。静态分析可以是保守的和合理的;然而，它可能是不准确的，可能产生弱的结果，并且可能需要明确的目标或注释。动态分析从程序执行中获取信息，例如proling和testing。动态分析使用程序执行期间计算的实际值，而不是对程序的状态进行建模。动态分析可以是高效和精确的，但结果可能无法推广到未来的程序执行。我们的研究将静态分析和动态分析结合起来，以利用它们的互补优势：动态分析可以提出由静态分析验证的程序属性本文主要对程序不变量进行分析程序不变式是在特定程序点为真的属性，例如可能出现在断言语句或形式规范中。不变量包括过程前置条件和后置条件、循环不变量和对象（表示）不变量。例子包括y=4x+3;x>abs（y）;数组a不包含重复;n = n.child.parent（对于所有节点n）;size（keys）=size（contents）;图g是非循环的。不变量解释了数据结构和算法，并有助于从设计到维护的编程任务。不变量有助于创建更好的程序[30，46，35，34]，文档程序操作[39，45]，协助测试并实现正确的修改[52，29]，协助测试用例生成[59]和验证[7]，形成程序谱[1，55，31]，并可以实现优化[6]，以及其他用途。尽管有其优点，但不变量通常在程序中缺失。动态不变量检测是一种用于从程序运行中假设可能的不变量的技术：动态不变检测器运行目标程序，检查它计算的值，并寻找这些值上的模式和关系，报告在整个测试套件上总是为真的那些，并满足某些其他条件（见2.1节）。输出可能是不变量：它们不能保证是普遍正确的，因为测试套件可能不会描述程序的所有可能执行静态不变式验证是一种检查程序属性的技术给定一个程序和该程序的一组属性，验证器报告哪些属性对于所有执行都保证为真。未验证的属性可能是也可能不是普遍正确的。静态验证器可以通过数据流分析、定理证明、模型检查或其他技术来操作。静态验证器的用户必须用要证明的属性（以及这些属性可能依赖的其他属性将动态不变检测与静态验证相结合，对于不变量检测器的用户和静态检查器的用户都是如此。因为3动态不变检测器的输出不能保证是声音的，程序员可能不愿意使用它，并且它的输出不能被馈送到需要声音输入的其它工具静态验证器可以指示哪些建议的不变量保证为真。 用户可以筛选出未验证的不变量，以便结果是合理的，或者在确定哪些动态检测属性是功能不变量，哪些是使用属性时，可以使用验证作为rst近似|这两种方法都很有用，但用于不同的任务。静态验证器的用户受益于减少的注释负担。静态验证通常需要大量的注释或中间断言和目标。 自动注释减轻了用户的注释负担-从头开始编程|很少有人喜欢或擅长的任务。动态检测的不变量还可以指示程序员可能忽略的属性。我们已经开始通过将动态不变检测器Daikon [16，17]与静态验证器ESC/Java [14，44]集成来探索这些好处。我们的系统分为三个步骤。首先，它运行Daikon，Daikon输出一个可能的不变量列表，这些不变量是通过在其测试套件上运行目标程序获得的。其次，它将这些不变量作为注 释 插 入 到 目 标 程 序 中 。 第 三 ， 它 在 带 注 释 的 目 标 程 序 上 运 行ESC/Java，以报告哪些可能的不变量可以静态验证，哪些不能。第4节提供了有关此过程的更多详细信息这三个步骤都是自动的。matic，但如果需要，用户可以提供指导以获得更好的结果。当发现缺陷时，用户可以编辑和重新运行测试套件，或者可以手动添加或删除特定的程序注释本文的其余部分组织如下。第2节提供了我们的系统所使用的动态不变检测器和静态验证器的背景。第3节介绍了几个实验的结果。第4节描述了我们如何集成这些工具，第5节讨论了在构建和运行我们的系统时出现的问题。最后，第6节将我们的研究结果与其他研究联系起来，第7节提出了后续研究，第8结束。2背景2.1Daikon：不变的发现动态不变量检测[16，17]通过检测目标程序来跟踪感兴趣的变量，在测试套件上运行检测程序，并在检测值上推断内变量，从而从程序执行中发现可能的不变量（图1）。推理步骤针对从仪表化变量捕获的值测试一组可能的不变量;那些被测试到足够程度而没有错误的不变量。阳离子报告给程序员。与其他动态方法一样，4测试套件原始程序仪表化程序仪器运行图1.一、Daikon实现的不变量动态检测概述例如测试和编程，推断的不变量的准确性部分地取决于测试用例的质量和完整性。Daikon invari- ant检测器与语言无关，目前包括C++和Java的仪器Daikon检测特定程序点的不变量，例如程序入口和出口;每个程序点都被独立对待。不变量检测器提供有变量跟踪，对于程序点的每次执行，该变量跟踪包含该点范围内所有变量的值。一组可能的不变量中的每一个都针对一个、两个或三个跟踪变量的各种组合进行测试。对于标量变量x、y和z，以及计算的常数a、b和c，检查的不变量的一些示例是：与常数（x = a）或一小组常数（x 2 f a;b;c g）相等，位于范围（aXb）、非零、模数（x a（mod b））、线性关系（z = ax + by +c）、排序（x y）和函数（x = fn（y））。涉及序列变量的不变量包括最小和最大序列值、字典序、元素序、序列中所有元素的不变量或成员资格（x2y）。给定两个序列，一些示例检查不变量是逐元素线性关系、字典比较和子序列关系。除了局部不变量，如node = node.child.parent（针对所有节点），Daikon还检测指向指针的数据结构上的全局不变量，如mytree通过线性化图形数据结构进行排序。最后，Daikon可以检测到不普遍为真的条件不变量，例如\if p6=null then p：value>x“和\p：value>limit或p：left2mytree“。条件不变量是根据条件将数据分割成部分并比较得到的不变量;如果两部分中的不变量不同，则它们被组合成条件不变量[19]。对于给定程序点处作用域中的每个变量或变量元组，测试每个潜在的不变量针对所有变量检查每个潜在的一元不变量，针对所有变量对检查每个潜在的二进制不变量，等等。通过检查每个样本来检查潜在不变量被测试的变量的值的元组）。一旦遇到不满足不变量的样本，则已知该不变量不成立，并且不检查任何后续样本。Daikon在程序大小增加时保持可接受的性能，因为假不变量往往不变量检测不变量数据跟踪数据库5很快就被证伪了，所以计算不变量的成本往往与发现的不变量的数量成正比。所有的不变量都是廉价的测试，不需要充分的定理证明。为了能够报告关于组件的不变量、聚集体的属性以及未存储在程序变量中的其他值，Daikon将这些实体表示为可用于推断的附加导出变量。例如，如果数组a和整数lasti都在作用域中，那么对[lasti]的属性可能会感兴趣，即使它不是变量，甚至可能不会出现在程序文本中。派生变量被不变检测器像对待其他变量一样对待，允许它推断出没有硬编码到其列表中的不变量。例如，如果size（A）是从序列A导出的，则系统可以报告不变量isize（A），而无需对标量和序列长度的情况下的小于比较检查进行<出于性能方面的考虑，只有在已知派生变量是合理的情况下才引入派生变量。例如，对于序列A，引入派生变量size（A），并在引入A[i]之前对其计算不变量，以确保i在A的范围内。一个不变量只有在有足够的证据证明其可解性时才被报告特别是，如果一个特定变量的样本数量不足，在它上面观察到的模式可能仅仅是巧合。因此，对于每个检测到的不变量，Daikon计算这样的属性在随机输入中偶然出现的概率。只有当其概率小于用户定义的置信参数时，才报告该属性[18]。Daikon不变量检测器可从http：//sdg下载。 lcs.mit.edu/daikon/。2.2ESC：静态检查ESC [13，14，43]是一个扩展的静态编译器，已经为Modula-3和Java实现。它静态地检测通常在运行时才检测到的常见错误，如空取消引用错误、数组边界错误和类型转换错误。ESC在功能和易用性方面介于类型检查器和定理证明器之间，但它的目标是更像前者，与后者相比是而不是证明完整的程序正确性，ESC只检测某些类型的错误。程序员必须编写程序注释，其中许多注释与断言状态类似，但在检查程序处理注释程序时，程序员不需要与检查程序交互。 ESC会发出关于无法证明的批注和潜在的运行时错误的警告。ESC执行模块化检查：它独立地检查程序的不同部分，并且可以检查部分程序或模块。它假定缺少或未检查组件的规范是正确的。ESC的实现在内部使用定理证明器。我们不讨论ESC6更详细地检查策略，因为这项研究将ESC视为黑盒（它以二进制形式分发）。ESC/Java是之前的ESC/Modula-3的继承者。ESC/Java的an-表示法语言（见4.2节）更简单，因为它稍微弱一点。这符合一个易于使用和对程序员有用的工具的哲学，而不是一个非常强大但使用起来非常困难的工具，程序员回避它。本研究使用ESC不仅作为一个轻量级的技术，用于检测一类有限的运行时错误，但也作为一个工具，用于验证表示不变量。我们选择使用ESC是因为我们不知道还有其他同样强大的技术可以静态检查可运行代码的属性鉴于许多其他验证器操作在非可执行的规范或模型，我们的研究旨在结合动态和静态技术在同一代码工件。此外，我们希望探索什么样的不变量可以动态检测和静态验证的限制。在任何情况下，通常需要良好的表示不变量来确定变量是非空的，数组访问是在范围内。ESC 的 两 个 版 本 都 可 以 从 www.example.com 公 开 获 得http://research.compaq。com/SRC/esc/.3实验本节给出了几个实验的定量和定性结果，静态验证动态检测的不变量。第3.1节和3.2详细讨论了从数据结构教科书中选取的两个例子[61];这些部分描述了生成的不变量，并提供了关于我们系统输出的直观信息。第3.3节概述了其他实验，并强调了系统可能遇到的问题类型。3.1StackAr：基于数组的堆栈StackAr示例是一个基于数组的堆栈实现[61]。源代码包含七个方法中的40行非注释代码，以及描述类行为但未提及其表示不变式的注释。我们的系统确定了表示不变量、方法预条件、修改目标和后置条件，并静态地证明了这些属性的成立。如果没有这些注释，ESC会发出关于许多潜在运行时错误的警告。通过添加检测到的不变量，ESC成功地检查StackAr类避免了运行时错误，满足了其规范，并在执行期间维护了重要属性图2显示了Daikon不变量检测器 nds 88不变量：6对象不变量，5个requires子句（方法前置条件），3个modi es子句（修改目标）和74个ensure子句（方法后置条件）。怎么--7可表达难以形容独一无二的雷顿独一无二的雷顿 总确保174001774对象60006需要40015莫迪是30003总304001888图二. Daikon在StackAr程序中检测到的不变量。该表通过可表达性（是否可以用ESCJML语言声明;见第4.2节）和冗余（是否逻辑上隐含其他不变量）对不变量进行我们的系统发现并证明了70个不变量，其中30个是非冗余的。有18个不变量在ESC中是无法表达的（见4.2节）。 还有，其他不变量隐含了58个不变量，可以通过Daikon中改进的冗余检查来删除（见第7节）。最后，我们的系统详细地添加了2个涉及数组所有者的注释（见4.3节）。图3显示了StackAr的自动注释源代码的一部分。前六个注释描述了表示不变量。数组永远不会为null，其运行时类型为Object[]。 topOfStack索引至少为1，并且小于数组的长度。最后，如果数组的元素的索引不超过topOfStack，则它们是非空的，否则为空。接下来的四个注释描述了构造函数的规范。 如果在入口处容量是非负的，那么在出口处数组长度匹配给定的容量，topOfStack索引指示空堆栈，并且数组的所有元素都为null。(The nal断言是多余的：它由表示不变量暗示。除了证明不存在错误外，我们的系统还生成了特定的类的所有操作，并验证实现满足规范。例如，topAndPop方法的两个后置条件是：/*@确保（\old（topOfStack）==-1）==（\result==null）*//*@ensure（\old（topOfStack）>=0）==（\result！= null）这些不变量声明topAndPop返回null当且仅当进入堆栈时堆栈为空方法的断言提供了部分规范，但不一定给出完整的输入输出关系。由于几个原因，从检测到的不变量导出的规格是有用的。首先，用户可以通过阅读特定的方法来理解方法的行为，阳离子，而不是推理的实施。 同样，静态工具8public class Uncategorized{/*@invariant this.theArray！= * //*@ invariant \typeof（this.theArray）== \type（java.lang.Object[]）*//*@invariant this.topOfStack>=-1 *//*@ 不变this.topOfStack< = this.theArray.length-1 *//*@invariant（\forall inti;（0=ii=this.topOfStack）==>（this.theArray[i]！= null））*//*@invariant（\forall inti;（this.topOfStack+1=i&&i<=this.theArray.length-1）==>（this.theArray[i]==null））*/public StackAr（intcapacity）/*@需要容量>=0 *//*@确保容量== this.theArray.length *//*@确保了这一点。topOfStack==-1 *//*@ensure（\forall inti;（0=ii=this.theArray.length-1）==>（this.theArray[i]==null））*/{new Object[ capacity]; topOfStack=-1;/*@set theArray.owner=this */}.../*@spec_public */ private Object [ ] theArray;/*@invariant theArray.owner==this *//*@spec_public */private int topOfStack;...}图三.带注释的StackAr.java的对象不变量、rst方法和eld声明 [61]。JML注释（以\/*@”开头的注释）由Daikon自动生成，由我们的系统自动插入到源代码中，并由ESC/Java自动验证可以检查断言，并且可以使用（检查的）断言来执行关于调用代码的响应此外，修改现有代码的程序员他们可以检查以前产生的规范，并在未经修改的程序上证明，在新的源上仍然有效。最后，invari- ants解释了实现的潜在重要属性。例如，StackAr上的表示不变量保证未使用的ar-ray元素被设置为空。因此，从堆栈弹出的对象不会被阻止被垃圾收集。9对象可表达独一无二的雷顿永远4 1 0无法形容的独特Redun。0 0总5需要14510020莫迪是200002确保. 14 - 40 1755117见图4。Daikon在DisjSets程序中检测到的不变量。该表通过可表达性（是否可以用ESCJML语言声明）、冗余性（是否逻辑上隐含其他不变量）和验证能力（ESC是否能够验证它）对不变量进行我们的系统发现并证明了80个不变量，其中34个不冗余。由于测试集的特殊性，两个巧合的不变量无法得到证明。3.2DisjSets：union- nd disjoint sets第二个例子进一步说明了我们的结果，并提供了一个例子的不变量，不能被验证。DisjSets类是不相交集合的基于数组的实现，它将整数范围划分为支持联合和查找操作的不相交子集[61]。源代码包含四个方法中的30行非注释代码，以及描述类行为但未提及其表示不变式的注释。我们的系统确定了表示不变量，方法前提条件，修改目标和后置条件，并静态证明了这些属性的大部分。图4显示Daikon在该类中发现了144个不变量;其中62个不变量在ESC中不可表达，其余46个是冗余的。同样，通过启发式方法添加了2个涉及数组所有者的注释。ESC证明了82个可表达的不变量中的80个，并警告了两个（不可证明的）测试套件工件。不可证明的不变量是用于检测不变量的测试套件的巧合在DisjSets实现中，s是用于表示集合的整数数组;s[i]引用同一集合中的另一个整数，或者如果元素是其集合的领导者，则为-1对于工会行动，Daikon报告了以下先决条件：/*@ 需要s[s.length-2]< 长度-1 */这个不变量表明倒数第二个元素的邻居永远不是最后一个元素。测试用例不包括倒数第二个元素被添加到最后一个元素的集合中的情况与此断言相矛盾的测试可以添加到套件中，但可以说不是通用的。总3446275514103.3其他实验我们已经在其他七个例子上运行了我们的系统，这些例子主要是从教科书和麻省理工学院编程课程中的STA解决方案到作业中选择的。我们选择这些特定的程序，因为它们包含有趣的，非平凡的表示不变量，没有明显超出ESC的能力。我们的系统无法验证所有检测到的这些其他程序的不变量（如StackAr）。第5节讨论了静态验证的挑战，但我们在这里简要说明了这些挑战我们发现有三大类问题。首先也是最重要的是测试套件的工件，它最初会导致许多不相关的（并且不是普遍正确的）不变量。例如，变量的整数边界，比如denom 19719720，是测试套件的常见工件。 最初的测试套件是来自教科书或用于评分的单元测试。我们推测，单元测试往往比典型的使用更小，更程式化，抛出了Daikon的统计公正测试（见第2.1节），这似乎在运行系统测试时工作得很好。第二类验证问题涉及Daikon无法检测的不变量|缺少不变量的类。例如，在有理数的否定方法中，Daikon检测到参数和结果的命名者相等证明该属性需要检测参数的分子和分母是相对素数，因此构造函数调 用的 gcd 操 作没 有 效 果。 我 们以 前 曾 拒绝 这 样的 不 变 量作 为insufficiently普遍适用性。然而，用户可以通过编写一个满足具有四个方法的接口的Java类来轻松地向Daikon添加不变量第三类问题涉及ESC无法证明某些内变量。我们发现，发现第二类和第三类问题的根源是容易和快速的，我们几乎没有麻烦说服自己的不变量或代码的正确或不正确。相比之下，扩展单元测试套件以发现Daikon输出中有趣的不变量是耗时且乏味的。在未来，我们将避免从单元测试开始。4执行本节讨论我们的实现。我们增强了Daikon的不变量检测能力，使其能够报告某些不变量（第4.1节）。为了允许ESC验证检测到的不变量，它们必须转换为ESC的输入语言（第4.2节）。最后，简要地添加了一些注释（第4.3节）。114.1白萝卜附加物我们对Daikon做了一些增强，使其输出更容易为ESC证明。我们在序列元素上添加了一些不变量，例如将所有元素与另一个变量或常量进行比较。这样的不变量出现在Daikon的前一个版本中[17]，但没有被添加到当前的实现中。我们列出了例程修改的变量 这种输出有时会产生误导。例如，disjoint-set union方法修改了s[set 2];但是set 2可能是0，所以s[0]也被列为可能被修改，即使它永远不会被修改，除非set 2是0。我们计划通过静态分析方法文本和从修改列表中删除与始终修改的变量重叠的有时修改的变量来消除这个无关的列表我们增强了Daikon的拆分标准列表，以考虑布尔过程返回值和过程退出点。Daikon使用这些标准通过将数据分成两部分来产生含义[19];如果不同的不变量在数据的部分中为真，则它们可以组合成含义或析取。因此，Daikon能够报告什么先决条件导致布尔函数返回true或false，或者什么先决条件导致执行某个return语句（以及其他属性）。最后，我们修改了Daikon，使其在对象不变量隐含非私有方法的不变量时不报告它们。尽管Daikon没有成功地将所有冗余的不变量都删除，但这大大减少了冗余报告的不变量的数量，使它们更易于管理，而无需删除任何信息。 输出的变化并没有影响不变量的可证明性，但确实简化了ESC的解释。输出.4.2ESC符号ESC的输入语言是Java建模语言JML的变体[41，42]。JML是一种接口规范语言，可以指定Java模块的行为。与我们的研究最相关的是它能够指定对象表示不变量和方法前提条件和后置条件。JML表达式的语法与Java非常相似。我们使用\ESC- JML”作为ESC/Java接受的JML变量的Daikon的默认输出语言也类似于Java，其扩展允许某些类型的不变量比Java更简洁或更清晰地表达。作为一个用户选项，Daikon可以在ESCJML中产生输出。这些格式之间的差异分为两类。当语义因为ESCJML不太方便或简洁而改变，但语言同样具有表达力时，我们通常将Daikon的输出转换为ESCJML。在ESCJML不能表达概念的情况下，12Daikon用自己的语言发现和表达，我们在尝试用ESC验证时省略了这些不变量。4.2.1语义差异（完整）JML和Daikon的默认输出格式都支持数组压缩，例如[i. j]来表示a的从索引i到j（包括i和j）的子数组。Daikon还允许通过表达式\arrayelements“进行量化;例如，this ：s elements this ：s：length。Daikon用子脚本符号a[i]统一简洁地表示对数组、向量和链表的访问。字段访问可以应用于序列，指示指定字段的序列;例如，a[].fld表示序列a[0].fld 、 a[1].fld 、 . 相比之下 ，ESCJML 通过显式 的\forallquanti er声明数组上的表达式，并且不能访问向量或链表元素。默认情况下，Daikon输出中的表达式仅在其子表达式合理时才被假定为有效例如，在Daikon的输出中，foo：bar=22表示\foo=null或foo：bar=22“，a[i]>x表示\i0或i a：length或a[i]>x“。<一个Daikon开关使这些警卫明确的输出或eliminates不变量的表达式，有时是无意义的。在ESC中，当i可能不是合法索引时，使用像a[i]这样的表达式可能会导致验证失败和无信息的错误消息。Daikon的对象不变量被指定在非私有方法的入口和出口处保持不变，而ESC被要求在所有方法的入口和出口处保持不变。但是，私有助手方法不需要要求或维护对象不变量。为了匹配语义，我们可以删除Daikon的对象不变量，并在所有适当的方法入口和出口处重复它们，但我们认为这太冗长和混乱;这阻止了ESC证明一些真正的（公共）对象不变量。4.2.2ESCJML中不可表达的不变量Daikon和ESCJML方法后置条件可以指示（通过Daikon中的orig（）或ESCJML中的\old（））表达式应该在前置状态下进行计算。例如，return=orig（x）表示过程返回x在方法被调用之前持有的值，即使过程可能在其执行期间修改了x。Daikon的orig（）可以应用于任何变量，并区分数组身份，数组内容和数组顺序。ESCJML的\old（）不能应用于数组内容或原始类型的方法参数。此外，没有办法将后状态的表达式与前状态的表达式混合在一起。(Some这些限制可以通过存在量化器等技巧来解决，但由此产生的不变量不是特别可读。ESCJML注释不能包含方法调用，即使是没有边带的方法调用。Daikon使用这些来获得Vector元素并作为蕴涵中的谓词。13与Daikon不同，ESCJML不能表示闭包操作，例如链表中的所有这些集合上的属性通常是递归定义的数据结构上最有趣和最重要的不变量完整的JML语言允许断言中的方法调用，\old（）应用于原始参数，\reach（）用于通过transi- tive闭包表示可达性4.3其他注释我们的系统通过spec_public注释使私有变量可以被指定访问。更重要的是，在每个构造器中，它将每个非原始eld的所有者ghost eld设置为正在构造的对象。这表明eld的内容不会被其他对象别名化。如果没有这个注释，ESC的理由是eld可以任意修改。在任何时候都可以用另一种方法来证明，而且几乎没有什么可以证明的。在不进行源代码分析的情况下添加此注释可能不安全，但这一原则经常被遵循，因此在我们迄今为止的实验中它是可以接受的。5挑战本节讨论动态检测程序不变量的静态验证的挑战。这些挑战分为三大类：工具的问题，目标程序的问题，以及目标程序的测试套件的问题。在有些情况下，我们基本上解决了问题，在另一些情况下，困难仍有待克服。5.1工具第4.1节列出了作为本研究一部分的Daikon不变检测器的增强功能。由于Daikon仍然是一个原型，我们预计未来可能需要额外的变化，特别是当它扩展到新的不变品种时。此外，加强对冗余不变量的检查将减少其输出的大小，并在不删除任何信息的情况下提高可理解性。第4.2节指出了ESC的输入语言的问题，这是JML的一个变体，它不能表达某些重要的不变量，也不能简洁清晰地表达其他不变量。在某些情况下，ESC似乎不足以验证某些真正的不变量，并且它的错误消息偶尔是神秘的。然而，总的来说，我们对ESC感到满意：它的运作有效而高效。例如，虽然我们没有在Daikon的源代码上运行ESC，但ESC已经在Daikon中检测到至少两个错误，因为它没有验证报告的不变量，经过仔细检查，这些不变量是不正确的。(Both错误是剪切和粘贴错误：在一种情况下，不变格式例程是不正确的，在另一种情况下，数组的第一个元素被忽略。14ESC不能表示字符串上的不变量，Daikon报告在任何情况下都很少有这样的不变量。因此，ESC无法证明对象不变量在解释字符串参数的构造函数或其他方法的出口处保持不变，即使它可以证明该不变量由其他方法维护。在少数情况下，ESC无法证明Daikon报告的属性，因为该属性依赖于超出Daikon范围的对象不变式。用户可以手动添加此类不变量，也可以删除依赖于它们的属性。5.2目标程序对不变量的静态验证的另一个挑战是，程序可能包含阻止所需不变量为真的错误。（虽然这从来不是我们的目标，但我们以前在教科书[30，61]和测试研究[36，56]中使用的程序中发现了这样的错误。作为我们在这个项目中检测到的一个可能的错误的例子，StackAr的一个对象不变量声明堆栈中未使用的元素为null;这允许在堆栈弹出后对对象进行垃圾收集，并允许更早地检测某些类型的错误。topAndPop操作维护这个不变量（这大约使其代码大小加倍），但makeEmpty例程无法做到这一点|一个不明显的疏忽，执行者和客户应该被评估。5.3测试套件动态不变量检测可以产生对于目标程序在其上运行的测试套件为真但对于程序的任意运行不为真的属性。然而，该问题通过将动态不变检测与静态验证相结合来解决。静态验证器表明，一些不变量是普遍真实的;其他可能是真的，但超出了验证器的能力，可能是真的程序总是运行的上下文，或者可能是测试套件的意外使用属性。在后一种情况下，报告的不变量指定了测试套件的非预期属性，使其不像它应该的那样通用，因此程序员确切地知道测试套件的错误以及如何改进。因为静态验证部分地解决了在所有上下文中哪些不变量必然为真的问题，所以本节的其余部分只在没有静态验证的情况下处理这个问题：从输出中消除所有不普遍为真的属性有多困难，以便它在没有任何警告的情况下验证？在某些情况下，“bad”不变量给出了关于需要添加到测试套件中的测试用例的有价值的提示。例如，在我们的一些实验中，某些堆栈操作没有在完全满的15堆栈，并且通过数组实现的队列不会通过添加和删除超过其容量的元素来强制回绕。作为另一个严重疏忽的例子，测试套件对安全堆栈弹出操作的调用总是受到数组是否为空的检查的保护。产生的输入变量表示结果始终为非空，表明未检测方法在其他情况下，然而，消除不受欢迎的不变量是一个繁琐的苦差事。它需要编写一个测试用例，该测试用例伪造了一个与抽象无关的特定特殊情况（它与特定实现的数据结构相关，但与逻辑无关）。最大的问题是不受欢迎的变量上限和下限我们推测，Daikon对这些特定不变量的统计检验需要调整。还有一种可能是，由于这些统计检验力求时间和空间效率，它们做了太多的近似，不能产生准确的结果。6相关工作这是我们所知道的第一个动态生成，然后静态证明，程序属性的研究。动态分析已经被用于各种任务;例如，归纳逻辑编程（ILP）[54，8]产生一组Horn子句（一阶if-then规则），并且可以在程序跟踪上运行[4]，尽管具有有限的可执行性。通过示例[12]进行编程是类似的，但需要密切的人类指导，并且版本空间可以兼容地表示假设集[50，33，40]。值proling [5，57，6]可以在运行时有效地检测某些简单的属性.事件跟踪可以生成nite状态机，用于解释潜在的系统组织或行为[9，10]。程序谱[1，55，31，2]还捕获了系统运行时行为的各个方面。这些其他技术都没有Daikon在检测程序中的不变量方面那么成功，尽管许多技术在其他领域很有价值。也存在许多静态推理技术，但由于篇幅所限，无法在此讨论它们。除了ESC之外，还有许多其他技术和工具用于静态检查正式规范[53，15，22，13，20，51，43]。这些其他系统有着与ESC不同的优点和缺点，但很少有系统能像ESC那样与真正的编程语言集成（见第7节）。6.1胡迪尼与我们最密切相关的研究是Houdini，一个ESC/Java的注释助手[24，23]。Houdini的动机是观察到用户不愿意用不变量注释他们的程序;它试图通过提供初始集来减轻负担。Houdini将候选注释集作为输入，并计算对特定16程序.它会反复调用检查器并删除被拒绝的注释，直到不再有注释被拒绝为止。候选不变量都是elds（和“有趣的常数”，如1，0，1，数组长度和null）之间可能的算术比较;这个初始集合的许多元素是相互矛盾的。Daikon的候选不变量比Houdini的候选不变量更丰富; Daikon输出蕴涵和析取，其基本不变量也更丰富，包括更复杂的算术和序列运算。如果有一个不变量缺失，那么Houdini会消除依赖于它的所有其他真的不变量。Houdini不会像Daikon那样尝试消除隐含的（冗余的）不变量（将其输出大小减少一个数量级最后，胡迪尼没有公开，所以我们不能进行直接比较。将这两种方法结合起来可能非常有用。例如，Daikon的输出可以形成Houdini的输入，允许Houdini花费更少的时间消除错误的不变量。（原型\动态反驳”|本质上是有限动态不变检测器|已建成[24]，但没有提供有关它的细节或结果。胡迪尼有一个不同的意图比Daikon：胡迪尼不试图产生一个完整的规范或注释，对人们有好处，但只是为了弥补缺失的注释，并允许程序不那么混乱;在这方面，它类似于类型推理。然而，Daikon的输出也许可以用来代替Houdini的。那些为真但依赖于缺失的不变量或不能被ESC证明的不变量将不会被消除，因此用户可能更接近于一个完全注释的程序，尽管他们可能需要手工消除一些不变量。7今后工作第5节列出了我们的系统（以及其组件Daikon和ESC）的一些问题，这些问题应该得到纠正。扩展这项工作的另一个明显的方法是使用不同的不变检测器比Daikon或不同的验证器比ESC。第6节列出了其他一些不变检测器。与真正的编程语言相关的静态验证器的例子包括LCLint [22，20，21]，ACL2 [38]，LOOP [37]，Java Path [32]和Bandera [11]。我们目前正在将Daikon与IOA [28，27]集成，IOA是一种用于描述使用I/O自动机[47，48，49]建模的计算过程的IOA 工具集（http：//theory.lcs.mit.edu/tds/ioa.html）允许IOA程序运行，并提供了一个接口到落叶松证明器（LP）[25，26，58]，一个交互式的多分类定理证明系统。一阶逻辑Daikon将提出目标、引理或中间断言给定理证明者 诸如表示不变量之类的附加条件可以17启用在所有可达状态/表示中保持的证明（但不在所有可能的状态/表示）。对于人们来说，指定要证明的属性可能是乏味和容易出错的，并且当前的系统在假设它们时有困难;一些研究人员认为这项任务比执行证明更难[60，3]。我们也有兴趣从静态验证失败的尝试中恢复。广义地说，验证失败是因为目标属性太强或太弱。太强的属性可能是真的，但超出了验证器的能力，或者可能不是普遍真的（例如，由程序上下文或测试套件的工件保证）。太弱的性质是真的，但不能被静态验证器证明或对它没有用处|例如，循环不变式可能需要被加强以被证明。我们预计，动态不变检测将提出更多的过于强大的不变量比过于薄弱的。当验证失败时，我们想知道如何通过检查源代码、程序执行、不变量模式和验证输出，以原则性的方式加强和削弱不变量，以增加成功验证的可能性虽然动态不变检测已经在一些应用领域相当成功，我们认为，真正成功的程序分析需要静态和动态组件。对一种分析来说很难的东西，对另一种分析来说很容易。 通过检查源代码，可以清楚地看到从动态分析中难以获得的一些属性，并且可以在运行时轻松检查静态分析中超出现有技术的属性。我们计划将更多的静态分析集成到我们的系统中（特别是Daikon）。动态分析不需要检查由静态分析发现的属性，并且动态分析可以集中于静态指示的代码。8结论我们已经证明了动态检测，然后静态验证，程序不变量的可行性。特别是，我们已经建立了一个系统，采取输出的Daikon不变检测器，并将其提供给ESC静态检查。据我们所知，我们的系统是第一个动态检测，然后静态证明程序属性。在小程序上的初步