|
| Tutor: |
Patrice Chalin |
Affiliation: |
Concordia University, Canada |
Date: |
August 21, 2006 |
Time: |
2:00-5:30, 1/2hr break at 3:30 |
Location: |
ITB 238 |
Format:
| 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.
|
| |
Topic:
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.
|
Objective:
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.
|
Prerequisites:
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:
http://secure.ucd.ie/products/opensource/ESCJava2/
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.
http://www.cs.iastate.edu/%7Eleavens/JML/papers.shtml
|
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.
|
