FMCO 2005 Tutorial Proposal
"Beyond Hoare Logic Assertions:
Advanced Specification and Verification with JML and ESC/Java2"

An FMCO 2005 Tutorial

Organizer: Joe Kiniry

Abstract

This tutorial introduces advanced aspects of JML annotation language and the ESC/Java2 extended static checker.

The Java Modeling Language (JML) is a formal behavioral interface specification language that can be used to specify the behavior of Java modules. It combines the Design by Contract approach of Eiffel and the model-based specification approach of the Larch family of interface specification languages, with some elements of the refinement calculus. JML has a Java-based syntax and semantics. Thus, it is easy to learn for Java programmers.

ESC/Java2 is a tool that checks that a program is consistent with its annotation. It also detects at compile time common programming errors that ordinarily are not detected until run time, and sometimes not even then; for example, null dereference errors, array bounds errors, type cast errors, and race conditions. While ESC/Java uses a theorem prover, it feels to a programmer more like a powerful type checker.

Because JML is familiar to Java programmers, and ESC/Java2 just feels like a typechecker, we believe that they are an excellent way to gently introduce programmers to formal methods.

Most specification languages, JML included, contain, at their core, assertion specification constructs familiar to most computer science undergraduate students: assertions, pre- and postconditions, class and loop invariants, etc. Unfortunately, these constructs have insufficient expressiveness to write specifications for programs written in languages like Java. The essential ingredients of a specification language for a modern object oriented language include a number of constructs which are unfamiliar to most students and practicianers, including frame axioms, ghost and model fields, and datagroups, and a complementary set of concepts with which a programmer must wrestle with, including aliasing, class invariants, and inheritance. This tutorial focuses on these constructs and concepts, explaining their meaning, purpose, and use for those familiar with the basic concepts of specification.

Attendee Background

Attendees are expected to be familiar with the basic constructs of Hoare Logic (assertions, pre- and postconditions, and invariants) and object oriented systems and their basic specification (a la Eiffel). Any Java programmer or researcher who wishes to improve the quality of their software, develop with or on JML or related tools, or learn about the state-of-the-art in OO program specification and verification should attend. Also, educators who want to use JML and ESC/Java2 in teaching, as a gentle way to introduce students to state-of-the-art specification and verification techniques and tools supporting formal methods, should also attend this tutorial.

Objectives

Attendees will come out of this tutorial with a firm understanding of advanced JML specification constructs in software design and engineering and will be knowledgeable about the various tools available for the JML language, particularly ESC/Java2 and the two Eclipse plug-ins available.

Duration

This tutorial was originally designed to be an all-day tutorial, as this will give instructors time to demonstrate the tools, interact with attendees, show various user-interfaces and options, etc. If necessary, it can be given as a half-day, or even 60-90 minute tutorial as well, though it will have correspondingly less, but more focused, content.

Tutorial History

Versions of this tutorial has been given at ECOOP 2004, ETAPS 2005, FM 2005, and ECOOP 2005, thus all course material is available immediately. In particular, extensive slides, homework assignments, and an ongoing book on JML and ESC/Java2 are available. Classes have also been given by two of the presenters at AIST and Eindhoven University of Technology.

Organizer Biographies

All presenters are experts on extended static checking, program verification, JML, Java, and related topics. Erik Poll, David Cok, and Patrice Chalin's attendance are not yet confirmed.

  • Joseph Kiniry, University College Dublin
    Joe is a Lecturer in the School of Computer Science and Informatics at University College Dublin. Previously he was a Postdoc in the SoS Group at the Radboud University Nijmegen. He earned his Ph.D. in Computer Science from the California Institute of Technology. Joe is a co-author and maintainer of ESC/Java2.
  • Erik Poll, Radboud University Nijmegen
    Erik is a Lecturer in the SoS Group at the Radboud University Nijmegen. He earned his Ph.D. in Computer Science from the University of Eindhoven.
  • David Cok, Eastman Kodak Company
    David is Chief Technologist for the Photographic Center within Kodak's R&D Laboratories in Rochester, New York. He earned his Ph.D. in Physics at Harvard University. He has participated in and led software development projects for research and commercialization. David is a co-author of ESC/Java2.
  • Patrice Chalin, Concordia University
    Patrice Chalin is an Assistant Professor in the Computer Science and Software Engineering Department of Concordia University, Montreal, where he is leading the Dependable Software Research Group. After the completion of his Ph.D. in Computer Science (from Concordia), he spent almost seven years in the telecommunications industry working in network application software development and software quality management.

Resources

The following resources are available for all interested in JML and ESC/Java, whether you decide to attend our tutorial or not. We will include tutorial material on this web page at a later date.