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

# Daikon FAQ (Frequently Asked Questions)

Contents:

- How can I get Daikon?
- What is Daikon?
- What is an operational abstraction?
- What is an operational abstraction good for?
- How is an operational abstraction used?
- How accurate is Daikon?
- How can I change my program to make Daikon work better?
- What does the name Daikon mean?
- What's new in Daikon?
- How can I get help? How can I learn more?
- How can I help?

## 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:

- Document code, indicating the structure of its data and computation.
- Maintain invariants to avoid introducing bugs; if a property is established at one point in a program, it is likely to be depended on elsewhere, but if the invariant is not documented, it is all to easy to accidentally violate it, introducing a bug in a far-removed part of the program.
- Locate unusual conditions that should be brought to a programmer's attention and may be bugs.
- Bootstrap proofs and aid static checkers by providing goals and automating the time-consuming, tedious chore of annotating programs.

Uses of invariants by other tools include:

- Check assumptions by converting the invariants to `assert` statements.
- Validate test suites by indicating the level of value coverage, which indicates how many different values are computed. This complements code coverage, which tells how many lines are executed.
- Provide hints for profile-directed compilation, but at the level of the program abstractions, permitting entire function calls to possibly be omitted after a check.

## 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.)

- Seeing the “w >= 0” invariant, the programmer might remark, “I already knew that w is non-negative; that doesn't help me.” (However, examining this invariant consumes little of the programmer's time.)
- Seeing the “x < 10” invariant, the programmer might realize after a moment's thought that the test suite is deficient: it never manipulates data structures containing more than 9 elements. This invariant has indicated not only a problem with the test suite, but exactly how to fix it.
- Seeing the “y = w + x” invariant, the programmer might suddenly understand the operation of the algorithm or why certain parts of the program are coded in the way they are. This can prevent long sessions of puzzlement over the system, and inserting the invariant as a comment can prevent others from going through the same confusion.
- Seeing the “z = 0 (mod 4)” invariant, the programmer might be confused about why z is always a multiple of 4. The programmer has two options.
  1. The programmer can examine the program and test suite to understand why this is so. (Perhaps z holds a pointer value or is some other kind of specialized index; perhaps it is a capacity that is always increased by a multiple of 4; perhaps there is some odd property of the test suite.) This gives the programmer a much better understanding of the operation of the program.
  2. The other option is for the programmer not to investigate this property further — perhaps it is not directly relevant to the current task — but to be careful not to make changes that violate that property. Violating the property could introduce errors if other parts of the code depend on it.

## 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 ]