A comparative study of programmer-written and automatically inferred contracts

ABSTRACT

Where do contracts - specification elements embedded in executable code - come from? To produce them, should we rely on the programmers, on automatic tools, or some combination?

Recent work, in particular the Daikon system, has shown that it is possible to infer some contracts automatically from program executions. The main incentive has been an assumption that most programmers are reluctant to invent the contracts themselves. The experience of contract-supporting languages, notably Eiffel, disproves that assumption: programmers will include contracts if given the right tools. That experience also shows, however, that the resulting contracts are generally partial and occasionally incorrect.

Contract inference tools provide the opportunity for studying objectively the quality of programmer-written contracts, and for assessing the respective roles of humans and tools. Working on 25 classes taken from different sources such as widely-used standard libraries and code written by students, we applied Daikon to infer contracts and compared the results (totaling more than 19500 inferred assertion clauses) with the already present contracts.

We found that a contract inference tool can be used to strengthen programmer-written contracts, but cannot infer all contracts that humans write. The tool generates around five times as many relevant assertion clauses as written by programmers; but it only finds around 60% of those originally written by programmers. Around a third of the generated assertions clauses are either incorrect or irrelevant. The study also uncovered interesting correlations between the quality of inferred contracts and some code metrics.

REFERENCES

• 1: CITADEL webpage. http://se.inf.ethz.ch/people/polikarpova/citadel.html.
• 2: EiffelStudio. Eiffel Software. http://www.eiffel.com/.
• 3: Traffic. http://traffic.origo.ethz.ch/.
• 4: M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: An overview. In CASSIS 2004, volume 3362 of LNCS. Springer, 2004.
• 5: Marat Boshernitsan , Roongko Doong , Alberto Savoia, From daikon to agitator: lessons and challenges in building a commercial tool for developer testing, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146258]
• 6: P. Chalin. Are practitioners writing contracts? In Springer LNCS 4157, pages 100--113, 2006.
• 7: Ilinca Ciupa , Bertrand Meyer , Manuel Oriol , Alexander Pretschner, Finding Faults: Manual Testing vs. Random+ Testing vs. User Reports, Proceedings of the 2008 19th International Symposium on Software Reliability Engineering, p.157-166, November 10-14, 2008 [doi>10.1109/ISSRE.2008.18]
• 8: Christoph Csallner , Yannis Smaragdakis, Check 'n' crash: combining static checking and testing, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062533]
• 9: Christoph Csallner , Yannis Smaragdakis, DSD-Crasher: a hybrid analysis tool for bug finding, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146267]
• 10: Michael Dean Ernst , David Notkin, Dynamically discovering likely program invariants, University of Washington, 2000
• 11: N. Gupta and Z. V. Heidepriem. A new structural coverage criterion for dynamic detection of program invariants. In ASE 2003: Proceedings of the 18th Annual International Conference on Automated Software Engineering, pages 49--58, Montreal, Canada, October 8-10, 2003.
• 12: Sudheendra Hangal , Monica S. Lam, Tracking down software bugs using automatic anomaly detection, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581377]
• 13: Michael Harder , Jeff Mellen , Michael D. Ernst, Improving test suites via operational abstraction, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
• 14: J. Henkel and A. Diwan. Discovering algebraic specifications from Java classes. In L. Cardelli, editor, ECOOP 2003 - Object-Oriented Programming, 17th European Conference, Darmstadt, July 2003. Springer.
• 15: Johannes Henkel , Amer Diwan, A Tool for Writing and Debugging Algebraic Specifications, Proceedings of the 26th International Conference on Software Engineering, p.449-458, May 23-28, 2004
• 16: Gary T. Leavens , Albert L. Baker , Clyde Ruby, Preliminary design of JML: a behavioral interface specification language for java, ACM SIGSOFT Software Engineering Notes, v.31 n.3, May 2006 [doi>10.1145/1127878.1127884]
• 17: Bertrand Meyer, Applying "Design by Contract", Computer, v.25 n.10, p.40-51, October 1992 [doi>10.1109/2.161279]
• 18: Bertrand Meyer, Object-oriented software construction (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1997
• 19: Jeremy W. Nimmer , Michael D. Ernst, Automatic generation of program specifications, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 20: Jeremy W. Nimmer , Michael D. Ernst, Invariant inference for static checking: an empirical evaluation, ACM SIGSOFT Software Engineering Notes, v.27 n.6, November 2002 [doi>10.1145/605466.605469]
• 21: C. Pacheco and M. D. Ernst. Eclat: Automatic generation and classification of test inputs. In ECOOP 2005 - Object-Oriented Programming, 19th European Conference, Glasgow, Scotland, July 25--29, 2005.
• 22: 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
• 23: B. Pytlik, M. Renieris, S. Krishnamurthi, and S. P. Reiss. Automated fault localization using potential invariants. In Proceedings of the Workshop on Automated and Algorithmic Debugging 2003, 2003.
• 24: N. Tillmann, F. Chen, and W. Schulte. Discovering likely method specifications. In ICFEM, pages 717--736, 2006.
• 25: J. W. Tukey. Exploratory Data Analysis. Addison-Wesley, Reading, MA, 1977.
• 26: T. Xie and D. Notkin. Tool-assisted unit test selection based on operational violations. Automated Software Engineering, 2003. Proceedings. 18th IEEE International Conference on, pages 40--48, Oct. 2003.
• 27: Hai Yuan , Tao Xie, Substra: a framework for automatic generation of integration tests, Proceedings of the 2006 international workshop on Automation of software test, May 23-23, 2006, Shanghai, China [doi>10.1145/1138929.1138942]

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Programming by contract

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Invariants; Pre- and post-conditions

General Terms:
Experimentation, Languages

Keywords:
dynamic contract inference, eiffel