Dynamic constraint detection for polymorphic behavior

ABSTRACT

Dynamic invariant detection, the automatic recovery of partial program specifications by inferring likely constraints from program executions, has been successful in the context of procedural programs. The implementation for dynamic invariant detection examines only the declared type of a variable, lacking many details in the context of object-oriented programs. This paper shows how this technique can be extended to detect invariants of object-oriented programs in the presence of polymorphism by examining the runtime type of a polymorphic variable, which may have different declared and runtime types. We demonstrate the improved accuracy of the dynamically detected specification on two real-world examples: the Money example from the JUnit testing framework tutorial, and a database query engine model example, which we adopted from a commercial database application. Polymorphic constraints in both cases are shown to reveal the specification of the runtime behavior of the systems.

REFERENCES

• 1: Daikon invariant detector. http://pag.csail.mit.edu/daikon.
• 2: Grady Booch, Object-oriented analysis and design with applications (2nd ed.), Benjamin-Cummings Publishing Co., Inc., Redwood City, CA, 1993
• 3: E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns. Addison-Wesley, 1995.
• 4: Jeff H. Perkins , Michael D. Ernst, Efficient incremental algorithms for dynamic detection of likely invariants, Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, October 31-November 06, 2004, Newport Beach, CA, USA
• 5: Jos Warmer , Anneke Kleppe, The object constraint language: precise modeling with UML, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1998

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Class invariants

General Terms:
Algorithms, Verification

Keywords:
automatic specification recovery, class invariants, dynamic invariant detection, object constraints