Quickly detecting relevant program invariants

ABSTRACT

Explicitly stated program invariants can help programmers by characterizing certain aspects of program execution and identifying program properties that must be preserved when modifying code. Unfortunately, these invariants are usually absent from code. Previous work showed how to dynamically detect invariants from program traces by looking for patterns in and relationships among variable values. A prototype implementation, Daikon, accurately recovered invariants from formally-specified programs, and the invariants it detected in other programs assisted programmers in a software evolution task. However, Daikon suffered from reporting too many invariants, many of which were not useful, and also failed to report some desired invariants.This paper presents, and gives experimental evidence of the efficacy of, four approaches for increasing the relevance of invariants reported by a dynamic invariant detector. One of them — exploiting unused polymorphism — adds desired invariants to the output. The other three — suppressing implied invariants, limiting which variables are compared to one another, and ignoring unchanged values — eliminate undesired invariants from the output and also improve runtime by reducing the work done by the invariant detector.

REFERENCES

• ECGN: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution, IEEE Transactions on Software Engineering, v.27 n.2, p.99-123, February 2001 [doi>10.1109/32.908957]
• EGKN99: Michael D. Ernst, William G. Griswold, Yoshio Kataoka, and David Notkin. Dynamically discovering pointerbased program invariants. Technical Report UW-CSE-99-11-02, University of Washington, Seattle, WA, November 16, 1999.
• Goe85: Amrit L. Goel. Software reliability models: Assumptions, limitations, and applicability. IEEE Transactions on Software Engineering, SE-11(12):1411-23, December 1985.
• Gri81: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• HFGO94: Monica Hutchins , Herb Foster , Tarak Goradia , Thomas Ostrand, Experiments of the effectiveness of dataflow- and controlflow-based test adequacy criteria, Proceedings of the 16th international conference on Software engineering, p.191-200, May 16-21, 1994, Sorrento, Italy
• OJ97: Robert O'Callahan , Daniel Jackson, Lackwit: a program understanding tool based on type inference, Proceedings of the 19th international conference on Software engineering, p.338-348, May 17-23, 1997, Boston, Massachusetts, United States [doi>10.1145/253228.253351]
• RH98: Gregg Rothermel , Mary Jean Harrold, Empirical Studies of a Safe Regression Test Selection Technique, IEEE Transactions on Software Engineering, v.24 n.6, p.401-419, June 1998 [doi>10.1109/32.689399]
• Sal68: Gerard. Salton, Automatic Information Organization and Retrieval., McGraw Hill Text, 1968
• Wei99: Mark Allen Weiss. Data Structures and Algorithm Analysis in Java. Addison Wesley Longman, 1999.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Invariants

General Terms:
Design, Experimentation, Measurement, Performance, Theory