内容发布更新时间 : 2024/5/7 20:34:34星期一 下面是文章的全部内容请认真阅读。

本科毕业论文（设计）

译文和原文

题作学专学

目 程序不变式检测工具的分析与应用 者 院 业 号

二〇一二年二月八日

计算机科学与技术 计算机科学与技术

指导教师

第一章 前言

程序不变量是在特定的一个或多个程序点上永保真值的属性，如可存在某一断言语句，形式化规格说明，或不变式的描述。例如Y=4*X+3；数组a不包含复制；n=n；子节点：父亲节点(给所有节点n)；size(key)=size(contents)；以及有向无环图。

不变量表明了程序的数据结构和变量运算规则，并且有利于程序的维护。例如，当修改代码时他们定义的程序属性必须保存。尽管有这些优势，不变量还是经常在编程中丢失。此外程序员应能从程序中自动推断出疑似不变量来充分注释代码。动态技术的研究专注于动态技术从运行的轨迹中发现不变量。一个程序不变量的动态检测是检查变量在一系列测试用例的值并记录在这些值中的属性和关系。

本章节讨论了如何获得不变量(1.1章节)，介绍动态不变量检测(1.2章节)，讨论关于两个与动态技术的运用有关的观点(测试集在1.3章节，属性的使用在1.4章节)，列举不变量的使用(1.5章节)，列举关于论文的贡献者(1.6章节)，给出其余文件的路线图(1.7章节)。

1.1 获取不变量的方法

程序员在写程序或者用其他方式操作程序时，应该有意识的加入程序不变量，因为这样可以很好的把握系统的运行情况，可以清楚的描述数据结构以及表达变量之间的关系等。但是比较可惜的是，这一主张在实际编码过程中几乎没有得到应用，因此大多数程序完全缺乏正式的或者非正式的不变量分析。

另一方面，程序员应在用不变量注释代码时能自动的推测出不变量。不变量检测包含在设计空间的隐藏部分：程序员脑海里所想的不变量。不变量检测是动态或静态的。

静态分析检测程序测试并找出可能的执行和运行时间状态。最普遍的静态分析是数据流分析，用抽象作为其理论解释依据。传统，健全的分析结果能保证所有可能的执行为真；由于编译器和其它一些系统不是面向用户，它在一些对正确性要求严格时非常合适。

静态分析有局限性。它不能真实的报告除了不可判定的属性或程序上下文的属性。在静态分析程序中运用了语言的特征，例由于堆栈近似值的精度缺失而难以表示并会产生较弱的结果，指针会余留在技术状态那边。动态分析在这些执行中运行程序，检查执行并报告属性，且不受这些缺点影响同时互补静态分析。

1.2 动态不变量检测

本研究主要专注动态发现不变量：这个技术是通过执行一个关于程序集的输入以

1

及从获得的不变量轨迹中推测出的不变量。图1.1显示的是以一亚洲人命名的不变量检测工具Daikon的高层体系结构。

动态不变量检测从程序执行中发现疑似不变量，通过指令目标程序去产生一些确定值，通过测试套件运行机器程序，推论编译的不变量并获得未在程序中显露不变量。

所有的步骤都是自动的（除了选择测试套件）。现在存在的工具是资源到资源翻译的C，Java，Lisp；我们使用的是工具和前后交互模式。

推论步骤测试可能的不变量对于那些从指令值获得的值。满足所有值，并能满足其它测试，例如数据合理性，不被相关联值，不被其它报告的不变量所包含的属性才称为可能不变量。

1.3运行程序

动态分析需要执行的目标程序。一个好的测试套件的好处大于它的花费，即使是没有动态不变量的检测下，它还能使用于其它动态技术例如（回归）测试。的确，一个程序缺少测试套件（不能运行或没有）可能会出现很多问题，并应在不变量检测前用标准技术来改正之。

与其它的动态测试或研究方法相比，推断不变量的准确性取决于测试用例的质量及理解性。额外的测试用例可能会提供一些新数据，以推断出更准确的不变量。推断的不变量可在执行时通过揭示属性为真来验证测试套件。这样，用户才知道这个测试套件是否足够，如果不是，则直接告知怎样改进它。

事实上，标准的测试套件是很合适的，且能从特别的相对不敏感套件中检测不变量，只要它足够大（参见第6章）。然而，我们还不知道确切的属性从而使测试套件能良好检测错误。这些不尽相同使测试套件能够检测缺陷。测试套件执行的效率如果是通用最小次数来执行每条语句，那么它对不变量检测不好，它需要重复的执行作为归纳基础，并有统计数据作为推论的支持。

在任何动态分析中，动态不变量检测都不能保证其结果的完整性或正确性。它不完整因为这可能报告出很多不确定的潜在不变量。然而，它又是完整的，因为它检查的不变量集；Daikon的语法在3.2节给出并在后面的论文中扩展，大多数在4.3节。它不准确因为测试套件不能列出所有的执行：存在前10000次执行后的属性不一定存在下一个里。然而，技术在这些训练数据（所有呈现的数据）又是准确的。

虽然动态不变量检测不够完整和准确，它还是很有用的，也是相当重要的财产。（这包括适合其它工具，例如测试，Purify[HJ92]，ESC[DLNS98],PREfix[PRE99]，等等。）此外，它能与其它工具互补；能弥补静态分析的缺陷，而静态分析也能覆盖它的缺陷。

1.4 功能不变量和使用性能

2