Download: PDF, Daikon implementation.
“Dynamically discovering pointer-based program invariants” by Michael D. Ernst, William G. Griswold, Yoshio Kataoka, and David Notkin. University of Washington Department of Computer Science and Engineering technical report UW-CSE-99-11-02, (Seattle, WA), November 16, 1999. Revised March 17, 2000.
Explicitly stated program invariants can help programmers by characterizing aspects of program execution and identifying program properties that must be preserved when modifying code; invariants can also be of assistance to automated tools. Unfortunately, these invariants are usually absent from code. Previous work showed how to dynamically detect invariants by looking for patterns in and relationships among variable values captured in program traces. A prototype implementation, Daikon, recovered invariants from formally-specified programs, and the invariants it detected assisted programmers in a software evolution task. However, it was limited to finding invariants over scalars and arrays. This paper presents two techniques that enable discovery of invariants over richer data structures, in particular collections of data represented by recursive data structures, by indirect links through tables, etc. 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. The second technique enables discovery of conditional invariants, which are necessary for reporting invariants over recursive data structures and are also useful in their own right. These techniques permit detection of invariants such as “p.value > limit or p.left in mytree”. The techniques are validated by successful application to two sets of programs: simple textbook data structures and student solutions to a weighted digraph problem.
Download: PDF, Daikon implementation.
BibTeX entry:
@techreport{ErnstGKN99,
author = {Michael D. Ernst and William G. Griswold and Yoshio Kataoka
and David Notkin},
title = {Dynamically discovering pointer-based program invariants},
institution = {University of Washington Department of Computer Science
and Engineering},
number = {UW-CSE-99-11-02},
address = {Seattle, WA},
month = {November~16,},
year = {1999},
note = {Revised March~17, 2000}
}