https://www.dagstuhl.de/09292

July 12 – 17 , 2009, Dagstuhl Seminar 09292

The Java Modeling Language (JML)

Organizers

Joseph Roland Kiniry (University College Dublin, IE)
Gary T. Leavens (University of Central Florida – Orlando, US)
Robby (Kansas State University, US)
Peter H. Schmitt (KIT – Karlsruher Institut für Technologie, DE)

For support, please contact

Dagstuhl Service Team

Documents

List of Participants
Dagstuhl Seminar Schedule [pdf]

Motivation

Program verification has been a topic of research interest far into the history of computing science. Today, it is still a key research focus, see e.g., Hoare’s Verified Compiler Grand Challenge and the Verified Software Initiative. A main facet in this effort is the ability to formally express properties that must be verified. Building on a long line of work in formal methods for reasoning about behavioral specifications of programs, several recent languages balance the desire for completeness and the pragmatics of checkability. In the context of the object-oriented programming paradigm, the Java Modeling Language (JML) is the most widely-adopted specification language in the Java formal methods research community.

The Java Modeling Language (JML) is a formal, behavioral specification language for Java. It describes detailed designs of Java classes and interfaces using pre- and postconditions, invariants, and several more advanced features. JML is used as a common language for many research projects and tools, including a runtime assertion checker (jmlc), tools to help unit testing (jmlunit), an extended static checker (ESC/Java), and several formal verification tools (e.g., LOOP, JACK, KRAKATOA, Jive, and KeY). JML is seeing some use in industry,particularly for financial applications on Java Smart cards and for verifying some security properties of a computer-based voting system.

Since JML is widely understood in the formal methods research community, it provides a shared notation for communicating and comparing many advances, both theoretical and practical, and it serves as a launching pad for research on advanced specification language features and tools. Researchers are using JML to study or express results for a wide variety of problems; these problems include verification logics, side effects (including frame axioms and modifies clauses), invariants, behavioral subtyping, null pointer dereferences, interfacing with theorem provers, information hiding, specifying call sequences in frameworks, multithreading, compilation, resource usage, and security. In addition to the tools mentioned above, JML is also used to express, compare, or study tools for checking specifications, unit testing, and specification inference. JML is used to state research problems for formal specification languages and for general discussions of specification language design. JML has also inspired at least three other similar specification languages, Spec#, BML, and Pipa, and has influenced the design and tools for Eiffel. Representatives of these communities are included in the invitation list. JML tools are used in the implementation of at least two other specification languages: ConGu and Circus. At present, there are at least 19 research groups around the world that are cooperating on JML-related research. These groups, and others, have published well over 100 papers directly related to JML (see www.jmlspecs.org/papers.shtml).

The seminar will pull together and energize the broad community of JML researchers and developers. We plan to have seminar participants work together on JML’s documentation, examples, pedagogical materials, and implementation infrastructure. The meeting will also provide a forum for considering changes to the language, for organizing community efforts, and for discussing recent work on formal methods relating to JML and its semantics. We plan to have fewer talks than an average Dagstuhl seminar and much more interaction and working sessions. We intend to involve the participants in writing documentation, examples, teaching materials, and library specifications. They will also discuss and debug software infrastructure and a novel semantics for JML. In addition, they will discuss and help organize the JML community.

Classification

  • Programming Languages/compiler
  • Semantics/formal Methods
  • Sw-engineering
  • Verification/logic

Keywords

  • Specification language
  • Formal methods
  • Verification

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.