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.
