Verification-centric Development in Java using
BON, JML, and ESC/Java2

A TOOLS 2008 Tutorial

Date: 1 July 2008
Time: 11:00-18:00

Organizer: Joe Kiniry
(with the assistance of David Cok, Fintan Fairmichael, Gary Leavens,
Erik Poll, and Dan Zimmerman)

Tutorial Lecturers: Fintan Fairmichael and Dan Zimmerman

Abstract

This tutorial introduces the BON specification language and BONc tool, the JML annotation language and tool suite, and ESC/Java2 via their integrated and interactive use within the Eclipse IDE.

BON is a high-level textual and graphical systems specification language. BON supports seamless, reversible system specification from concept, requirements, and feature analysis all the way down to formal contracts of object-oriented and structured systems. BONc is a tool suite for using the BON specification language. It currently supports parsing, typechecking, and generating XHTML documentation for BON specifications.

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 (1) BON is a simple language which has the look-and-feel of English, (2) JML is familiar to Java programmers, and (3) ESC/Java2 just feels like a typechecker, we believe that they are an excellent way to gently introduce programmers to formal methods.

ESC/Java2 and JML have been deeply integrated into the Eclipse development environment, under the auspices of the European Union Framework 6 research program "Mobius". Within this large research project, many tools and technologies have been integrated to construct the Mobius Program Verification Environment (PVE), a customized version of Eclipse. The PVE looks and feels like Eclipse, but has numerous capabilities that helps one focus on program analysis, design, development, testing, verification, and maintenance using hidden, powerful static checkers, theorem provers, and more. BONc will be integrated into a future version of the PVE.

Attendee Background

Any Java programmer who wishes to improve the quality of their software should attend. Also, educators who want to use BON, JML, and/or 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 BON and JML specification languages, and will be knowledgeable about the various tools available for the BON and JML languages, particularly BONc and ESC/Java2.

Justification

Applied formal methods, as exemplified by the BON, JML, and ESC/Java2 work, are exactly within the purvey of TOOLS, thus this tutorial is of great relevance to TOOLS attendees. Additionaly, BON comes from the Eiffel community, and the design of some aspects of JML was influenced by the design of Eiffel's specification constructs.

Duration

This tutorial is an all-day tutorial, as this gives the instructors time to demonstrate the tools, interact with attendees, show various user-interfaces and options, etc.

Tutorial History

This tutorial has been presented to over a hundred academics and several hundred undergraduate and postgraduate students over the past several years. The first version of this tutorial was one of the most successful tutorials at ECOOP 2004, thus all course material is available immediately. In particular, extensive slides, homework assignments, and an ongoing book on JML and ESC/Java2 are available. Revised versions of this tutorial have also been given at several other top academic conferences, including ECOOP, ETAPS, FM, and FMCO.

Organizer Biographies

  • Joseph Kiniry, University College Dublin
    Joe is a lecturer in the School of Computer Science and Informatics at University College Dublin. He was previously in the SoS Group at Radboud University Nijmegen. He earned his Ph.D. in Computer Science from the California Institute of Technology. Joe is the coauthor of ESC/Java2 and has contributed to, or led the development of, several other verification tools.
  • Gary Leavens, University of Central Florida
    Gary is a Professor in the School of Electrical Engineering and Computer Science, University of Central Florida. Gary is the creator of the Java Modeling Language and leads the development of the JML Tool Suite.
  • Erik Poll, Radboud University Nijmegen
    Erik is a Lecturer in the SoS Group at Radboud University 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.
  • Fintan Fairmichael, University College Dublin
    Fintan is a PhD student working under the supervision of Joe Kiniry. He is the architect and author of the BONc tool suite. He earned a BSc in Computer Science at University College Dublin with first class honors in 2005 and an M.Sc. with distinction at the University of Oxford. Fintan is an IRCSET fellow.
  • Dan Zimmerman, University of Washington, Tacoma
    As inventor of the Dynamic UNITY formalism, Daniel M. Zimmerman received a Ph.D. in Computer Science from the California Institute of Technology for his work in formal methods for distributed systems design and development in 2002. Dan is an Assistant Professor at the University of Washington, Tacoma.

Resources

The following resources are available for all interested in BON, 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.