2026-03-09

Dynamically discovering likely program invariants to support program evolution

Year: 1999
Authors: Michael D. Ernst, Jake Cockrell, William G. Griswold, David Notkin
DOI: 10.1145/302405.302467

Persistent Notes

Daikon can extract invariants from arrays and scalars.S
This papers attempts to extend to other data structures
- The first method is convert any data structure to an array and run daikon on it
- The second methods detects conditional invariants over recursive data structures

In-text annotations

“A prototype implementation, Daikon, recovered invariants from formallyspecified programs, and the invariants it detected assisted programmers in a software evolution task. However, it was limited to finding invariants over scalars and arrays." Page 1

“The first technique is to traverse these collections and record them as arrays in the program traces; then the basic Daikon invariant detector can infer invariants over these new trace elements." Page 1

“1 Introduction” Page 1

“The instrumenter explicitly records in the trace file collections that are implicit (e.g., pointer-based). It does so by traversing the collection and writing out the visited objects as an array. We call this process linearization." Page 1

“conditional invariants (invariants that are not universally true” Page 1

“2 Background” Page 2

“the accuracy of the inferred invariants depends in part on the quality and completeness of the test cases." Page 2

“Because false invariants tend to be falsified quickly, the cost of computing invariants tends to be proportional to the number of invariants discovered." Page 2

“For instance, if array a and integer lasti are both in scope, then properties over a[lasti] may be of interest, even though it is not a variable and may not even appear in the program text." Page 2

“For performance reasons, derived variables are introduced only when known to be sensible. For instance, for sequence A, the derived variable size(A) is introduced and invariants are computed over it before A[i] is introduced, to ensure that i is in the range of A." Page 2

“Consequently, for each detected invariant, Daikon computes the probability that such a property would appear by chance in a random input. The property is reported only if its probability is smaller than a user-defined confidence parameter." Page 2

“3 Invariants over collections” Page 3

“Our approach is to extend the instrumenter to find collections that are implicit in the program, linearize them, and record them explicitly in the trace file as arrays." Page 3

“If a field is found that leads from an object to another object of the same type (e.g., element.next), the instrumenter outputs the two objects as successive elements in the same array. If there are multiple fields with this property (e.g., a prev field in addition to the next field), then one linearization is done for each field and multiple arrays are written into the trace file." Page 3

“Invariants over collections can be classified as either local invariants or global invariants." Page 3

“4 Conditional invariants” Page 3

“Many important program properties are not universally true." Page 3

“Conditional invariants are particularly important for programs that manipulate recursive data structures, because different properties typically hold in the base case and in the recursive case." Page 3

“The mechanism for detecting conditional invariants is to split data traces into parts based on some predicate, perform invariant inference on each part” Page 3

“We implemented the static analysis policy of using boolean expressions in a method and side-effect-free zeroargument boolean member functions;" Page 4

“5 Assessment” Page 4

“Our measure of quality for an invariant is relevance” Page 4

“5.1 Textbook data structures” Page 4

“For each of the classes in these programs for the selected test suite, Daikon reported at least 95% of the relevant invariants. For example, LinkedList reported 1 irrelevant invariant and 11 invariants that were implied by other reported invariants, meaning that 96% of the reported invariants were relevant. Daikon also never reported fewer than 98% of the expected invariants. For LinkedList, 3 manually identified relevant invariants were missed and 317 were reported, meaning that 99% of the manually identified invariants were found by Daikon." Page 4

“5.1.1 Qualitative analysis” Page 5

“Linked lists." Page 5

“We do not, however, detect the exact predicate for determining when deletion was successful. The reason is that we currently split only on conditions in the program (however, the current prototype does examine local variables, which often appear in conditionals) and zeroargument boolean member functions." Page 6

“Ordered lists” Page 6

“Stacks: list representation." Page 6

“Stacks: array representation” Page 6

“Queues” Page 6

“5.2 City map student programs” Page 7

“6 Incremental processing” Page 8

“After briefly discussing performance issues, we outline our approach to using online, incremental invariant inference to permit scaling Daikon to larger, more realistic programs." Page 8

“The former number tends to be relatively small, whereas the latter is cubic in the number of variables in scope at a program point." Page 8

“A straightforward approach to scaling is to give programmers control over instrumentation." Page 8

“To make the remaining tracing and inference go faster, we can eliminate I/O costs by running the invariant detector online in cooperation with the program under test, directly examining its data structures." Page 8

“When testing invariants online, we need not store all data values indefinitely. Values need only be accumulated initially to permit instantiating all viable invariants in a staged fashion, then discarded." Page 8

“7 Related work” Page 9

“Checking formal specifications” Page 9

“8 Conclusion” Page 9

%% Import Date: 2026-03-09T11:32:40.280-04:00 %%