FM 2005 Tutorial
"Design by Contract and Automatic Verification for Java with JML and ESC/Java2"
Morning of Tuesday, 19 July, 2005
Organizers: Joe Kiniry, Erik Poll, and (tentatively) David Cok
Abstract
This tutorial introduces the new ESC/Java version 2 and the JML annotation language.
The Java Modeling Language (JML) is a 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 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.
Attendee Background
Any Java programmer who wishes to improve the quality of their software 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 the use of specifications in software design and engineering, a basic knowledge of the JML specification language, and will be knowledgeable about the various tools available for the JML language, particularly ESC/Java2.
Duration
This tutorial is a half-day tutorial. This means we will only be able to give a brief introduction to JML and ESC/Java2 and a brief demonstration of the tools. Students or other interested parties can find any of the speakers during the week at FM 2005 for additional information, demonstrations, etc.
Tutorial History
This tutorial was one of the most successful tutorials at ECOOP 2004 and ETAPS 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. This tutorial is also being given at ECOOP 2005 a week later.
Organizer Biographies
- Joseph Kiniry, University College Dublin
Joe is a lecturer in the Deparment of Computer Science at University College Dublin. He was previously in the SoS Group at the University of Nijmegen. He earned his Ph.D. in Computer Science from the California Institute of Technology. Joe is the coauthor of ESC/Java2. - Erik Poll, University of Nijmegen
Erik is a Lecturer in the SoS Group at the University of Nijmegen. He earned his Ph.D. in Computer Science from the University of Eindhoven. - David Cok, Eastman Kodak Company
David is a Director of the Imaging Science Division 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 the co-author of ESC/Java2 and an expert on program verification, JML, Java, and related topics.
Registration
FM registration is open now. The registration form is available via the FM 2005 web site.
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.
- Primary Tools for the Tutorial
- ESC/Java2:
https://www.kindsoftware.com/products/opensource/ESCJava2/
- The JML tool suite:
https://www.jmlspecs.org/
- ESC/Java2:
- Papers
- For a good overview of JML and the tools available, read An Overview of JML Tools and Applications
- For background, history, and motivations of the design of JML, see JML: Notations and Tools Supporting Detailed Design in Java
- For an overview of using JML to support Design by Contract in Java, see Design by Contract with JML
- Many other papers on JML and related tools are available via the JML papers web page.
- Slides
- Introduction to JML (4 up)
- ESC/Java2: Use and Features (4 up)
- ESC/Java2 Warnings (4up)
- Specification Tips and Pitfalls (4 up)
- Advanced JML (and more Tips and Pitfalls) (4 up)
- ESC/Java: Extended Static Checking for Java (a summary and non-interactive demonstration)
- Effectively Using JML: Software Engineering Processes incorporating Formal Specification
- Using ESC/Java2 Architecture, Hints, and Tricks
- Using Formal Methods for VLSI Development: Using Java and JML in the Real World
- Models are the `M' in JML: Using ADT Models in Formal Specification with JML
- The ESC/Java2 Calculi and Object Logics: Implications on Specification and Verification
- Homework
- JML and ESC/Java Homework Exercises (learning JML and ESC/Java2 through hands-on work)