Contents:

Overview

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:

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 daikon-developers@pag.csail.mit.edu, post to the forums, or ask a CSE331 staff member.

Running Daikon

We provide an Ant target for running Daikon. It will work for any problem set:

    cd ps1
    ant daikon

(You should not run ant daikon until after ant test executes with no test failures.)

ant daikon 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:

  1. Executing target program: ...
    This is output to assist with debugging.
  2. The output of the target program itself. For Problem Set 1, this is a series of dots indicting successful completion of the JUnit test cases. You will notice that this runs slower than the original test. That is because it is generating a trace file.
  3. Progress output from Daikon. This starts with Executing daikon: and ends with Exiting Daikon.
  4. A message indicating that textual results are available in daikon.inv.txt.

Serialized (.inv) files

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.

Understanding the invariants

Program points

Daikon's output is organized in terms of program points, which are locations in the source code. Daikon has four types of program points:

Invariant syntax

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.