JML: Advancing Specification Language Methodologies

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 is 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.