Daikon is an implementation of dynamic detection of likely invariants. An invariant is a property (such as "x=2*y+5" or "this.next.prev = this" or "myarray is sorted by <") that holds at a certain point or points in a program. Invariants are often seen in assert statements, documentation, and formal specifications. Invariants can be useful in program understanding and a host of other applications. Daikon runs a program, observes the values that the program computes, and then reports properties that were true over the observed executions. It can detect properties in Java, C, C++, Perl, and IOA programs, in spreadsheet files, and in other data sources.

Changes

This release was enhanced to better support program points that are basic blocks. Some minor enhancements and bugfixes were made, and the documentation was improved.

URL: The Daikon dynamic invariant detector