摘要
明确声明的程序不变量可以帮助程序员识别修改代码时必须保留的程序属性。然而，在实践中，这些不变量通常是隐式的。期望程序员使用不变量对代码进行完全注释的另一种方法是自动从程序本身推断可能的不变量。本研究的重点是从执行跟踪中发现不变量的动态技术。本文报告了三个结果。首先，它描述了动态发现不变量的技术，以及体现这些技术的名为Daikon的实现。其次，报告了Daikon在两套目标计划中的应用。在Gries的程序推导工作中，系统重新发现了预定义的不变量。在缺少显式不变量的C程序中，系统发现了有助于软件演化任务的不变量。这些实验表明，至少对于小程序来说，不变推理是准确和有用的。第三，它分析了可伸缩性问题，如不变检测运行时和准确性，以及测试套件和程序点的功能。
介绍
本研究的重点是不变量的动态发现：该技术是对输入集合执行一个程序，并从捕获的变量轨迹推断不变量。图1显示了Daikon不变检测器的结构。与其他动态方法（如测试和分析）一样，推断不变量的准确性部分取决于测试用例的质量和完整性；额外的测试用例可能会提供新的数据，从中可以推断出更精确的不变量。
Daikon的Lisp instrumenter（第8节）添加了将变量值写入数据跟踪文件的代码；该代码自动插入程序入口（ENT