The Daikon invariant detector reports properties that hold at procedure entries and exits. The reported properties are similar to those in specifications or assert statements: representation invariants, preconditions ("requires" clauses), or postconditions ("effects" clause). Examples include "x == abs(y)", "i < myArray.length", or "myArray is sorted". These invariants can be useful in program understanding, testing, and a host of other applications.
Daikon runs your program, examines the values your program computes, and uses machine learning to find patterns and relationships among those values. Daikon reports properties that were true for all the executions that it observed.
Daikon's output differs from the specifications that you write in two important ways:
Daikon's output may contain properties that the true specification does not. (In other words, Daikon's output may be stronger (more specific) than the true specification.)
Daikon reports what it observed during execution, but properties may be true of a given execution (especially of a poor test suite) that are not true in general. For example, Daikon may report that all arguments to a procedure are positive. Maybe they truly must be positive, or maybe your test suite is poor, and it should really pass negative values to the procedure.
Daikon's output may be missing some properties that appear in the true specification. (In other words, Daikon's output may be stronger (more specific) than the true specification.)
Daikon can only report a limited number of properties; its learning algorithm is not as powerful or clever as the human mind.
Despite these limitations, Daikon's output is often a remarkably close approximation of the specification, and examining Daikon's output can assist you in understanding problems with your test suites, your specifications, or your code.
You can obtain more information about Daikon from its website. In particular, you can read its manual (HTML, PDF). If you have any problems with Daikon, please send mail to firstname.lastname@example.org, post to the forums, or ask a CSE331 staff member.
We provide an Ant target for running Daikon. It will work for any problem set:
cd ps1 ant daikon
This produces a representation invariant (also called an object invariant) for each class, and pre- and post-conditions for each method. This can be quite a bit of output, so for Problem Set 1 we have also supplied an Ant target that reduces the amount of output (and changes a few of the file names). See the Problem Set 1 handout for more details.
This target creates three files:
When you run the target, you will see four things:
Running Daikon both produces textual output (daikon.inv.txt) and also outputs the invariants in serialized (binary) form (daikon.inv.gz). You can use the daikon.inv.gz file to print the invariants:
java daikon.PrintInvariants daikon.inv.gz
Or, you can insert the invariants as comments in your Java source program (in as many or as few files as you like):
java daikon.tools.jtb.Annotate daikon.inv.gz src/ps1/RatNum.java src/ps1/RatPoly.java src/ps1/RatPolyStack.java
The Daikon website has an example of code after invariant insertion.
Daikon's output is organized in terms of program points, which are locations in the source code. Daikon has four types of program points:
Daikon uses its own syntax for outputting program properties. Some of the properties will be easy to interpret, but others may be confusing.
The variable orig(x) refers to the original value of formal parameter x — that is, its value on entry to the method. orig() variables appear only at EXIT program points.
Negative array indices count backwards from the length of the array; for instance, a[-1] denotes the last element of array a; it is just syntactic sugar for a[a.length-1].
The Daikon manual explains more conventions for variable names and for other aspects of Daikon output.