FM 2006

August 21 - 27, 2006
McMaster University
Hamilton ON, Canada

Submission Dates

Technical Papers, Workshops and Tutorials

Friday February 24, 2006

Posters and Tools, Doctoral Symposium

Friday May 26, 2006


Notification Dates

Technical Papers

Friday April 28, 2006

Workshops and Tutorials

Friday March 10, 2006

Doctoral Symposium

Wednesday June 14, 2006

Posters and Research Tools

Monday June 12, 2006

Contact Information

General Inquiries

General Chair

Emil Sekerinski

Program Chairs

Jayadev Misra,
Tobias Nipkow

Workshops Chair

Tom Maibaum

Tutorials Chair

Jin Song Dong

Tools & Poster Chair

Marsha Chechik

Industry Day Chairs

Volkmar Lotz,
Asuman Suenbuel

Doctoral Symposium Chair

Ana Cavalcanti

Augusto Sampaio

Jim Woodcock

Sponsorship Chair

Jürgen Dingel

T4 JML & ESC/Java2
Patrice Chalin
Concordia University, Canada
August 21, 2006
2:00-5:30, 1/2hr break at 3:30
ITB 238
Half-day, interactive.
Participants are welcomed to bring their own computers, and to download the tutorial slides as well as install the JML package. For those who cannot bring their own computer, lab computers will be provided.


This tutorial offers a practical and applied introduction to Design by Contract (DBC) for Java using the Java Modeling Language (JML). JML is a behavioral interface specification language that extends Java with support for DBC and non-null annotations, among other features. It has a Java-based syntax and semantics and is therefore easy to learn for Java programmers. Participants will be shown, and given an opportunity to work with, the most popular JML tools, namely: the JML compiler, ESC/Java2, and JmlUnit. The JML compiler offers support for the run-time checking of JML specifications. ESC/Java2, is an extended static checker that provides a compiler-like interface to fully automated checking of JML specifications. Like similar tools, ESC/Java2 compromises soundness and completeness for efficacy and utility. JmlUnit is a tool for generating JUnit test suites using JML specifications as test oracles. This tutorial will allow participants to get an appreciation for JML, and how these three main tools can help developers write accurate specifications and correct code.


Attendees will come out of this tutorial with first hand experience in using JML to write contracts for Java code while using run-time and compile-time checkers to “debug” specifications and formally verify the correctness of code.


Attendees are expected to be experienced with Java program development, and familiar with the basics of Design by Contract (assertions, method pre- and postconditions, and class invariants). The intended audience is Java developers wishing to make use of DBC, or educators interested in teaching applied DBC for Java.

Tutorial Resource Materials
• Primary Tools for the Tutorial
o Java 1.4 JRE or SDK installed.
o Eclipse 3.2
o ESC/Java2:
o The JML tool suite: jml-fm06.tar.gz
o For installation instructions see Section 2 of the tutorial notes. Can you please install this package and perform the "Tutorial setup sanity check" as outlined in the notes.
• Papers
o For a good overview of JML and the tools available, read An Overview of JML Tools and Applications
o For background, history, and motivations of the design of JML, see JML: Notations and Tools Supporting Detailed Design in Java
o For an overview of using JML to support Design by Contract in Java, see Design by Contract with JML
o Many other papers on JML and related tools are available via the JML papers web page.

Biography of Tutor:

Patrice Chalin is an Assistant Professor in the Computer Science and Software Engineering Department of Concordia University, Montreal, where he is head of the Dependable Software Research Group (DSRG), a leading contributor to the evolution of JML and its tools. 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.