目录:
概述
Daikon不变式探测器 报告在一个程序的某一点上所具有的特性。所报告的特性是一个算术公式，像你可以写一个断言性语句，如前置条件("requires" 子句), 或后置条件 ("effects" 子句)一样；例如, "x == abs(y)" or "i < myArray.length"。这些不变式在理解程序和许多其它的应用软件中是有用的。通过运行程序来操作 Daikon，测试它所计算的值，在那些值之间寻找模式和联系。
在 6.170锁中Daikon为你提供帮助。没有任何变量的情况下运行daikon将显示有用的信息 ：
athena% daikon
用法: daikon [OPTIONS] <MAIN CLASS> [MAIN ARGUMENTS]
选项:
-o, --output FILE Save invariants in FILE.inv
...
在最小值，你必须命名一个"main"类，这个类提供方法 "public static void main(String[] args)"，Daikon 将运行这个类测试你的程序。通过查看命令行选项段可以为daikon寻找详细的可用资料。
-
- -o, --输出 FILE
- 不变式在FILE.inv 中保存，在FILE.src.tar.gz中获取。如果之前没有给它们命名，则系统自动产生一个命名，并投入使用。
- -t, --文本文件
- 不变式的文本列表保存为文本文件。
- -v, --详细的
- 显示程序运行时的信息。
- -c, --清除
- 开始之前，从中断处删除剩余的文件。但只有当daikon发现有剩余文件并通知你去使用这个选项时，才能进行清除。
- -n, --没有用户界面
- 创建不变式文件 (如果系统提供此功能，最好创建为文本文件)，但不要开始运行 GUI。
The GUI (Graphical User Interface图形用户界面) 显示一个树状结构的结果视图。第一层，它显示审查之后的一个系列类， 每一个类又延伸出一系列程序点。
一个程序点通常与源代码中的一个特殊位相关联。例如，foo()结点之下的ENTER点代表进入foo()方法的前置条件。
ENTER和EXIT程序点识别给定方法的出入点，从客户或用户的观点看，OBJECT程序点指出表示不变式 (有时称为对象不变式)支持给定类的任何对象。这些特性从类的每个公用的方法进出时都有效。CLASS程序点很像对象程序点，但仅仅适用于静态变量。
显示不变式的一些句法很容易混淆。
在输出中, orig(x) 对到变量x 的应用是指引用形式参数的原值，orig() 变量仅仅出现在EXIT程序点。
负数数组指明从数组长度往后的计数，例如，a[-1] 表示数组 a中的最后一个元素；它仅仅是a[a.length-1]的句法表示 。
如果上面给定的方法对大多数用户来说是有效的，当然一些人也许想让它得到更进一步的开发。这一节描述的是在没有精装原稿的帮助的情况下如何使用 Daikon 。 这样做的原因之一是它让你控不变式检测(例如，哪个类已经测试过，哪个类还没有测试)。第二个好处是不用每次重新开始整个程序，你便可以编辑和重新提交一些文件。最后，通过运行个别的步骤，你将更好的理解在实际情况下程序的运行。
检测不变式包括以下三个步骤：
- 创建程序来增加输出变量的指令 。
- 运行程序 (也许可以使用一个测试套具)来创建数据痕量文件。
- 在数据痕量文件上运行 Daikon
不变式检测器来检测不变式。
Step 1:用工具规范程序
前端之所以修改你的程序，除了执行它最初的任务外，同时还给一个数据痕量文件写变量值。从1.0版到 1.3版，Java™在课程提纲、日程安排、讲义、作业、测试、读物、实验部分/复习、使用工具、以及项目等方面的编码前端工作与各种版本的Java™相关语言保持一致 。
在你的Java™课程提纲、日程安排、讲义、作业、测试、读物、实验部分/复习、使用工具、以及项目等方面的源文件上运行Java的前端Daikon--dfej，结果如下：
dfej filename1.java filename2.java ...
Java™课程提纲、日程安排、讲义、作业、测试、读物、实验部分/复习、使用工具、以及项目等方面的前端Daikon完成下面两件事：
- dfej给 daikon-java/目录写文件的版本
- dfej 在 daikon-output/ 目录中创建名为 filename1.decls, etc的说明性文件。
只有专业的 Java™ 课程提纲、日程安排、讲义、作业、测试、读物、实验部分/复习、使用工具、以及项目等文件实现了运行；其它文件只能手工运行。这将允许你控制不变式检测的作用域。
例如编译生成文件：
javac daikon-java/*.java
在一些测试套具上运行程序是为了创建数据痕量文件的采集。可以用你以前的方式运行工具程序；唯一变化的是在daikon-output/子目录（如果子目录不存在就创建一个）中写一个 .dtrace文件。当程序已经运行之后，即使已经创建了大量的.decls 文件（为每个源文件创建），也要创建一个唯一的.dtrace文件。
检测之后，有两个版本的程序：源版和出现在daikon-java/ 目录中的运行版本。 确信在目录包含源 Java™的 课程提纲、日程安排、讲义、作业、测试、读物、实验部分/复习、使用工具、以及项目编码之前，daikon-java/ 目录出现在你的类路径中。你可以在那个目录中运行此程序，看"." (当前目录)是否一开始就出现在你的类路径中，或者是否能精确地在你的类路径中添加daikon-java/目录。
运行完你的 Java™ 课程提纲、日程安排、讲义、作业、测试、读物、实验部分/复习、使用工具、以及项目等应用程序之后，在做为结果的 .dtrace文件上运行modbit-munge.pl ：
modbit-munge.pl myprog.dtrace
这一步解决了痕迹文件中的一些潜在问题。
通过命令运行 Daikon
不变式检测器
java daikon.Daikon decl-files... trace-files...
decl-files 说明 (.decl) 文件是在检测时间创建的。trace-files作为数据痕量 (.dtrace) 文件是通过运行工具程序创建的 。为了能包含所有对特殊数据痕量文件所需的说明性文件，最简单的办法是在运行在读程序时包含所有创建的说明性文件。
在系统默认的情况下，Daikon 能产生出一个不变式的文本列表来规范终端输出；但它也能用-o选项产生一个文件装载在 GUI里：
java daikon.Daikon -o foo.inv decl-files... trace-files...
此时，你得在文件中运行 GUI ：
java daikon.gui.InvariantsGUI foo.inv
Daikon主页
返回项部