An integrated verification environment for JML: architecture and early results

ABSTRACT

Tool support for the Java Modeling Language (JML) is a very pressing problem. A main issue with current tools is their architecture: the cost of keeping up with the evolution of Java is prohibitively high: e.g., almost three years following its release, Java 5 has yet to be fully supported. This paper presents the architecture of JML4, an Integrated Verification Environment (IVE) for JML that builds upon Eclipse's support for Java, enhancing it with Extended Static Checking (ESC), an early form of Runtime Assertion Checking (RAC) and JML's non-null type system. Early results indicate that the synergy of complementary verification techniques (being made available within a single tool) can help developers be more effective; we demonstrate new bugs uncovered in JML annotated Java source---like ESC/Java2---which is routinely verified using first generation JML tools.

REFERENCES

• 1: W. Ahrendt, T. Baar, B. Beckert, R. Bubel, M. Giese, R. Hähnle, W. Menzel, W. Mostowski, A. Roth, S. Schlager, and P. H. Schmitt, "The KeY Tool", Software and System Modeling, 4:32--54, 2005.
• 2: G. Barthe, L. Burdy, J. Charles, B. Grégoire, M. Huisman, J.-L. Lanet, M. Pavlova, and A. Requet, "JACK: a tool for validation of security and behaviour of Java applications". Proceedings of the 5th International Symposium on Formal Methods for Components and Objects (FMCO), 2007.
• 3: Lilian Burdy , Yoonsik Cheon , David R. Cok , Michael D. Ernst , Joseph R. Kiniry , Gary T. Leavens , K. Rustan M. Leino , Erik Poll, An overview of JML tools and applications, International Journal on Software Tools for Technology Transfer (STTT), v.7 n.3, p.212-232, June 2005 [doi>10.1007/s10009-004-0167-4]
• 4: L. Burdy, M. Huisman, and M. Pavlova, "Preliminary Design of BML: A Behavioral Interface Specification Language For Java Bytecode". Proceedings of the Fundamental Approaches to Software Engineering (FASE), vol. 4422 of LNCS, pp. 215--229, 2007.
• 5: 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.
• 6: P. Chalin and P. James, "Cross-Verification of JML Tools: An ESC/Java2 Case Study". Proceedings of the Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE), Seattle, Washington, August, 2006.
• 7: P. Chalin and P. James, "Non-null References by Default in Java: Alleviating the Nullity Annotation Burden". Proceedings of the 21st European Conference on Object-Oriented Programming (ECOOP), Berlin, Germany, July-August, 2007.
• 8: P. Chalin, P. R. James, and G. Karabotsos, "The Architecture of JML4, a Proposed Integrated Verification Environment for JML", Dependable Software Research Group, Concordia University, ENCS-CSE-TR 2007--006. May, 2007.
• 9: D. R. Cok, "Design Notes (Eclipse.txt)", http://jmlspecs.svn.sourceforge.net/viewvc/jmlspecs/trunk/docs/eclipse.txt, 2007.
• 10: D. R. Cok, E. Hubbers, and E. Rodríguez, "Esc/Java2 Eclipse Plug-in", http://sort.ucd.ie/projects/escjava-eclipse/, 2007.
• 11: 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.
• 12: C. Engel and A. Roth, "KeY Quicktour for JML": www.key-project.org, 2006.
• 13: M. Ernst and D. Coward, "Annotations on Java Types", JCP.org, JSR 308. October 17, 2006.
• 14: Michael D. Ernst , Jeff H. Perkins , Philip J. Guo , Stephen McCamant , Carlos Pacheco , Matthew S. Tschantz , Chen Xiao, The Daikon system for dynamic detection of likely invariants, Science of Computer Programming, v.69 n.1-3, p.35-45, December, 2007 [doi>10.1016/j.scico.2007.01.015]
• 15: Cormac Flanagan , K. Rustan M. Leino, Houdini, an Annotation Assistant for ESC/Java, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.500-517, March 12-16, 2001
• 16: James Gosling , Bill Joy , Guy Steele , Gilad Bracha, Java(TM) Language Specification, The (3rd Edition) (Java (Addison-Wesley)), Addison-Wesley Professional, 2005
• 17: Mikoláš Janota , Radu Grigore , Michal Moskal, Reachability analysis for annotated code, Proceedings of the 2007 conference on Specification and verification of component-based systems: 6th Joint Meeting of the European Conference on Software Engineering and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, p.23-30, September 03-04, 2007, Dubrovnik, Croatia [doi>10.1145/1292316.1292319]
• 18: Gary T. Leavens, Tutorial on JML, the java modeling language, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA [doi>10.1145/1321631.1321747]
• 19: 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, 2007.
• 20: 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, Languages, Theory, Verification

Keywords:
Eclipse, JML4, integrated verification environment, java modeling language