Early detection of JML specification errors using ESC/Java2

ABSTRACT

The earlier errors are found, the less costly they are to fix. This also holds true of errors in specifications. While research into Static Program Verification (SPV) in general, and Extended Static Checking (ESC) in particular, has made great strides in recent years, there is little support for detecting errors in specifications beyond ordinary type checking. This paper reports on recent enhancements that we have made to ESC/Java2, enabling it to report errors in JML specifications due to (method or Java operator) precondition violations and this, at a level of diagnostics that is on par with its ability to report such errors in program code. The enhancements also now make it possible for ESC/Java2 to report errors in specifications for which no corresponding source is available. Applying this new feature to, e.g., the JML specifications of classes in java.*, reveals over 50 errors, including inconsistencies. We describe the adjustment to the assertion semantics necessary to make this possible, and we provide an account of the (rather small) design changes needed to realize the enhancements.

REFERENCES

• 1: John Barnes , J. G. Barnes, High Integrity Software: The SPARK Approach to Safety and Security, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2003
• 2: L. Burdy, A. Requet, and J.-L. Lanet, "Java Applet Correctness: A Developer-Oriented Approach". Proceedings of the International Symposium of Formal Methods Europe, vol. 2805 of LNCS. Springer, 2003.
• 3: Patrice Chalin, Logical Foundations of Program Assertions: What do Practitioners Want?, Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, p.383-393, September 07-09, 2005 [doi>10.1109/SEFM.2005.26]
• 4: P. Chalin, "Reassessing JML's Logical Foundation". Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs (FTfJP'05), Glasgow, Scotland, July, 2005.
• 5: P. Chalin, "De-risking the Verifying Compiler Project: Recovering Soundness", Dependable Software Research Group, Department of Computer Science and Software Engineering, Concordia University, ENCS-CSE-TR 2005--009, 2006.
• 6: P. Chalin, J. Kiniry, G. T. Leavens, and E. Poll, "Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2". Fourth International Symposium on Formal Methods for Components and Objects (FMCO'05), 2005.
• 7: D. R. Cok and J. R. Kiniry, "ESC/Java2: Uniting ESC/Java and JML". In G. Barthe, L. Burdy, M. Huisman, J.-L. Lanet, and T. Muntean editors, Proceedings of the International Workshop on the Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS'04), Marseille, France, March 10--14, vol. 3362 of LNCS, pp. 108--128. Springer, 2004.
• 8: R. DeLine and K. R. M. Leino, "BoogiePL: A Typed Procedural Language for Checking Object-Oriented Programs", Microsoft Research, Technical Report, 2005.
• 9: D. L. Detlefs, G. Nelson, and J. B. Saxe, "A Theorem Prover For Program Checking", Compaq SRC, Research Report 159, 2002.
• 10: Robert Bruce Findler , Matthias Felleisen, Contract Soundness for object-oriented languages, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.1-15, October 14-18, 2001, Tampa Bay, FL, USA
• 11: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 12: D. Gries and F. B. Schneider, "Avoiding the Undefined by Underspecification", in Computer Science Today: Recent Trends and Developments, vol. 1000, J. v. Leeuwen, Ed.: Springer-Verlag, 1995, pp. 366--373.
• 13: Jim Grundy, Predicative Programming - A Survey, Proceedings of the International Conference on Formal Methods in Programming and Their Applications, p.8-25, June 28-July 02, 1993
• 14: C. A. R. Hoare and J. He, Unifying Theories of Programming. Prentice Hall, 1998.
• 15: Cliff B. Jones, Systematic software development using VDM (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 16: C. B. Jones and C. A. Middelburg, "A Typed Logic of Partial Functions Reconstructed Classically", Acta Informatica, 31(5):399--430, 1994.
• 17: J. R. Kiniry, P. Chalin, and C. Hurlin, "Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification". Proceedings of the International Conference on Verified Software: Theories, Tools, Experiments (VSTTE), Zürich, Switzerland, October 10--13, 2005.
• 18: B. Konikowska, "Two Over Three: A Two-Valued Logic for Software Specification and Validation Over a Three-Valued Predicate Calculus", Journal of Applied Non-Classical Logics, 3:39--71, 1993.
• 19: Beata Konikowska , Andrzej Tarlecki , Andrzej Blikle, A three-valued logic for software specification and validation, Proceedings of the 2nd VDM-Europe Symposium on VDM---The Way Ahead, p.218-242, August 1988, Dublin, Ierland
• 20: P. G. Larsen and N. Plat, "Introduction to Overture". First Overture Workshop, Newcastle upon Tyne, UK, July, 18, 2005.
• 21: G. T. Leavens, "JML's Rich, Inherited Specifications for Behavioral Subtypes", Department of Computer Science, Iowa State University, Ames, Iowa. USA, TR #06--22, 2006.
• 22: G. T. Leavens and Y. Cheon, "Design by Contract with JML", www.jmlspecs.org, 2006.
• 23: Gary T. Leavens , Yoonsik Cheon , Curtis Clifton , Clyde Ruby , David R. Cok, How the design of JML accommodates both runtime assertion checking and formal verification, Science of Computer Programming, v.55 n.1-3, p.185-208, March 2005 [doi>10.1016/j.scico.2004.05.015]
• 24: G. T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. Cok, P. Müller, J. Kiniry, and P. Chalin, "JML Reference Manual", http://www.jmlspecs.org, 2006.
• 25: K. R. M. Leino, "Ecstatic: An object-oriented programming language with an axiomatic semantics". Fourth International Workshop on Foundations of Object-Oriented Languages, January, 1997.
• 26: K. R. M. Leino, J. B. Saxe, and R. Stata, "Checking Java programs via guarded commands", COMPAQ SRC, Palo Alto, CA, SRC Technical Note 1999--002. 21 May 1999, 1999.
• 27: C. Marché, C. Paulin-Mohring, and X. Urbain, "The Krakatoa tool for certification of Java/JavaCard programs annotated in JML", Journal of Logic and Algebraic Programming, 58(1--2):89--106, 2004.
• 28: Bertrand Meyer, Applying "Design by Contract", Computer, v.25 n.10, p.40-51, October 1992 [doi>10.1109/2.161279]
• 29: Bertrand Meyer, Object-oriented software construction (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1997
• 30: Joseph M. Morris, Non-deterministic expressions and predicate transformers, Information Processing Letters, v.61 n.5, p.241-246, March 14, 1997 [doi>10.1016/S0020-0190(97)00023-9]
• 31: Mary Shaw , David Garlan, Software architecture: perspectives on an emerging discipline, Prentice-Hall, Inc., Upper Saddle River, NJ, 1996
• 32: J. M. Spivey, The Z notation: a reference manual, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 33: SRI International, "The PVS Specification and Verification System", http://pvs.csl.sri.com.
• 34: Joachim van den Berg , Bart Jacobs, The LOOP Compiler for Java and JML, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.299-312, April 02-06, 2001

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Design, Documentation, Languages, Theory, Verification

Keywords:
JML, extended static checking, java modeling language, precondition errors, specification debugging