daikon用户手册

http://plse.cs.washington.edu/daikon/download/doc/daikon.html

1 引言

Daikon是对可能的不变量的动态检测的实现；也就是说，Daikon不变量检测器报告可能的程序不变量。不变量是指在程序中的某一点或几点保持的属性；这些属性经常出现在断言语句、文档和正式规范中。不变量在程序理解和其他许多应用中都很有用。例子包括’x.field > abs(y)’；‘y = 2*x+3’；‘数组a被排序’；对于所有列表对象lst，‘lst.next.prev = lst’；对于所有treenode对象n，‘n.left.value < n.right.value’；‘p != null => p.content in myArray’；还有很多。你可以扩展Daikon以添加新的属性（参见增强Daikon输出，或参见Daikon开发者手册中的新不变式）。

动态不变式检测运行一个程序，观察程序计算的值，然后报告在观察到的执行过程中为真的属性。Daikon可以检测C、C++、C#、Eiffel、F#、Java、Perl和Visual Basic程序中的属性；电子表格文件；以及其他数据源中的属性。(动态不变量检测是一种机器学习技术，可以应用于任意数据)。将Daikon扩展到其他应用程序也很容易。

Daikon可以从download-site免费下载。Daikon的许可证允许不受限制的使用（见许可证）。该版本包括源代码（也可在GitHub上获得）和文档，许多研究人员和从业人