Daikon logo

[ Home | FAQ | Download | Documentation | Publications | Mailing lists ]


Daikon FAQ (Frequently Asked Questions)

Contents:

How can I get Daikon?

Daikon is available for download, including source code, binaries, and documentation, at http://plse.cs.washington.edu/daikon/download/.

What is Daikon?

Daikon is an invariant detector. Given a data source (such as the values computed by a program at run time), Daikon generalizes over the observed values and reports properties that are true about the data. Daikon implements a type of machine learning to summarize the raw data into a small set of easily comprehensible formulas.

What is an operational abstraction?

The set of formulas that Daikon outputs is called an operational abstraction. The operational abstraction states properties about a program's data structures — the sort that might be written in an assert statement or a formal specification.

Here is a simple example of Daikon's output: StackAr.html. The colored annotations starting with “@” (in JML format) were automatically detected by Daikon and automatically inserted in the source code. Many other uses for invariants are possible in addition to insertion as documentation.

What is an operational abstraction good for?

Program properties (such as specifications and dynamically detected invariants) are useful for a wide variety of software construction, understanding, reuse, and modification tasks. The properties may be examined by a human or used as input to a tool

Direct uses of invariants by a human include:

Uses of invariants by other tools include:

How is an operational abstraction used?

An operational abstraction can be used automatically, in which case a human never directly examines it, or both automatically and manually, in which case a human does examine (parts of) it. A number of automatic uses are discussed in the research papers that use Daikon.

As an example of manual use of Daikon, a programmer might run it on a program and see, at a procedure entry,

  w >= 0
  x < 10
  y = w + x
  z = 0 (mod 4)

(These examples are all numeric for simplicity, but Daikon detects relationships over general data structures, including arrays, collections, and pointers.)

How accurate is Daikon?

The Daikon system examines the values computed during the target program's execution, looking for patterns and relationships among those values. There are two potential problems: missing properties (false negatives), and spurious properties (false positives).

False negatives are inevitable, because every tool has a grammar that limits what it can express. Daikon has a relatively simple and broadly applicable grammar. Users can extend it easily, by writing a Java class that satisfies an interface with four methods.

False positives can also occur; the properties are not guaranteed to hold for every possible execution. As with any other dynamic (run-time) technique, such as testing, the results depend on the quality of the test suite. In practice, the results have proved to be quite accurate even with very modest test suites, thanks to statistical tests that weed out most false positives. And research has shown that the inaccuracies can help in improving test suites.

How can I change my program to make Daikon work better?

Another way of stating this question is, “On what sort of programs does Daikon tend to perform poorly?”

Typically, users will not run Daikon on a whole program, but on the particular component(s) of interest. Trying to run Daikon on too much data will overwhelm either Daikon, or else you when you try to examine the output. (If you plan to feed the output into another tool, verbosity is less of a concern.)

Daikon can produce invariants if you provide it with the appropriate values. If your data structures are organized in a fashion that makes Daikon unable to access those values, then Daikon obviously cannot produce any desired output. If values are packed (for instance, using a bit array instead of an array of boolean values), then Daikon will not be able to access the values. If values have very complex names (for example, a.b[i].c.d(), then Daikon may not even try that variable name. See the configuration options that control what derived variables Daikon uses.

What does the name Daikon mean?

A daikon is a type of Asian radish. Daikon is pronounced like the two English words die-con. The name can be thought of as standing for “dynamic conjectures”.

What's new in Daikon?

The CHANGELOG.md file lists what is new in each release of Daikon.

Before you report a bug, please upgrade to the latest version of Daikon to verify that the problem still exists, and then include all the information requested by the manual.

How can I get help? How can I learn more?

If you have questions about using Daikon, first read the Daikon manual, including the “Troubleshooting” section. If you have questions about modifying Daikon, also see the Daikon developer manual, the Javadoc API documentation, and the source code.

If you do not find an answer in the documentation, or you think you have found an error (bug), then use one of the mailing lists to get help from other Daikon users and from the Daikon developers. The manual tells you what information to include in your bug report in order to make it most useful, which maximizes your chances of receiving a fast and relevant reply.

How can I help?

Daikon is a collaborative project. Over two dozen programmers have contributed code (and we gratefully accept new features and bug fixes), and many users have helped by making suggestions and filing problem reports (whether about the code or the documentation). Please give us feedback through the mailing lists, or just tell us how you have used Daikon.


[ Home | FAQ | Download | Documentation | Publications | Mailing lists ]