JML: Advancing Specification Language Methodologies
23-27 March 2015
The Java programming language is by far the most popular object-oriented programming language, and the most popular programming language in teaching. The Java Modeling Language (JML) aims at providing uniform means to describe and establish formal correctness of Java programs. JML is being developed as a decentralised community project since around 1999. It is an annotation language based on the principle of design-by-contract, where classes are formally specified with invariants and single class methods are specified with pre- and post-conditions. Although design-by-contract is commonly associated with classical imperative approaches to formal verification based on Hoare logic and calculus, the verification techniques based on JML go considerably beyond this classical paradigm.
In the past years, JML has matured and is known to a broad audience of software engineering practitioners, researchers, university teachers and university students. There are several different methodologies for (more or less formal) verification. JML is now being applied in real-time, embedded, and concurrent systems; and for properties which go beyond functional correctness such as information flow security.
The research goals centred around JML are (i) to advance the art of specification and verification, (ii) to define and clarify the semantics of specifications in order to unify verification, and (iii) to make the JML based verification methods more practical. The practicality factor is especially important in university education, where the verification principles should be in focus. Following its title, “JML: Advancing Specification Language Methodologies”, our Lorentz Center workshop was dedicated to:
● further develop the design of JML and JML-like languages, in particular targeting the challenge of accommodating different specification and verification philosophies, as well as the different programming and execution platforms,
● unify the corresponding research efforts scattered around the world,
● share experiences and develop ideas for teaching formal specification and verification using JML and similar paradigms.
The workshop took roughly four and a half days with most participants staying the whole duration of the workshop. Generally, the program was divided 50/50 between scientific presentations (typically 30 minutes slots) and plenary discussions. Additionally, we had one short remote session with two participants from the United States (Daniel Zimmerman and Joseph Kiniry of Galois) who could not attend the workshop in person, but had very interesting insights about the use of JML in industrial context.
With respect to discussions, we initially planned on having discussions about: (a) teaching of JML and formal methods, (b) a book about JML, (c) tools, (d) design and standardisation of JML, and (e) industrial context. Discussions on topic (a) and (b) took place more or less as planned, however, during the course of the workshop the discussions on topic (d) took over most of the time allocated for the remaining topics. This was for a good reason and cause, as shortly described below. On Friday afternoon, the workshop was concluded by a one hour quiz about Java and JML intricacies to finish the week in a relaxed yet focused fashion.
The most important part of the workshop outcome was setting up the task force (in the persons of James Hunt and Mattias Ulbrich) for organising and cleaning up the JML standard. During the scientific presentations by the representatives of the different research groups it became apparent that there is a lot of disagreement and unclarities about the semantics of the JML language, and hence corresponding (very heated) discussions emerged. The different aspects of JML were discussed one by one over the course of the workshop and specific participants were appointed to write a summary, distribute it, and progressively put the discussed changes into effect.
During the discussions and work on the potential book on JML a preliminary list of contents for the book was established, and the editors for the book were initially appointed. Since the standardisation of the JML language is one of the prerequisites for the book, the book is one of the motivating factors for the work described above. A similar conclusion was developed in the sessions on JML in teaching. The participants emphasized the need for a more stable language and more stable tools supporting it. Many courses would benefit from a textbook.
Finally, it was decided that a follow-up meeting should take place in about a year time, the KIT research group preliminarily agreed to lead and organise such a meeting in Germany next year.