Lambda the Ultimate

Daikon

Daikon is an implementation of dynamic detection of likely invariants; that is, the Daikon invariant detector reports likely program invariants. An invariant is a property that holds at a certain point or points in a program; these are often seen in assert statements, documentation, and formal specifications. Invariants can be useful in program understanding and a host of other applications. Examples include “.field > abs(y)”; “y = 2*x+3”; “array a is sorted”; “for all list objects lst, lst.next.prev = lst”; “for all treenode objects n, n.left.value < n.right.value”; “p != null => p.content in myArray”; and many more. You can extend Daikon to add new properties (see Enhancing Daikon output).

Dynamic invariant detection runs a program, observes the values that the program computes, and then reports properties that were true over the observed executions.

Daikon can detect properties in C, C++, Java, Perl, and IOA programs; in spreadsheet files; and in other data sources. (Dynamic invariant detection is a machine learning technique that can be applied to arbitrary data.) It is easy to extend Daikon to other applications; as one example, an interface exists to the Java PathFinder model checker.

I spend a lot of time here talking about static typing, but let's face it: most often we're dealing with existing code that probably isn't written in a language with a very expressive type system, and rarely has been formally specified, whether through an expressive type system or otherwise. Daikon is interesting because it attempts to learn important properties of a piece of software by execution and observation. Combine it with a model checker like Java PathFinder, and you have an unusually powerful means of evolving the correctness of even quite complex code. There's also a relationship to the already-mentioned JML and ESC/Java 2, which in turn has a connection to the popular JUnit unit-testing framework. In short, the gap between compile time and runtime, and static vs. dynamic typing, seems to be narrowed in powerful ways by these, and related, tools.