JML — Java Modeling Language

A Quick Reference for JML, the Java specification language.

What is JML
JML Statements
JML conditions syntax

1. What is JML

The Java Modelling Language (JML) is a specification language for Java.

JML follows the Design-by-Contract Programming Paradigm: this means that it describes pre/post conditions of code that must be respected in order to get the correct and expected behavior.

The JML code is evaluated by JML Program Verification Tools (the most famous is OpenJML) that checks if the Java code meets or not the given JML rules. By a more formal point of view: Evaluating JML means checking if the java code violates the contract (see contract programming).

2. JML Statements

As JML is still not officially supported by Java, all the JML statements must be written inside comments.

JML statements are always referred to a specific Java Class (or method), so they must be written inside of the main class brackets. When they refer to a specific method, they must be written inside the method brackets just below the declaration (before variables and methods declaration).

Common JML statements

//@assignable: list of variables (divided by comma) that can change value during method execution (=mutable variables). If no mutable variables exist in the class, use the reserved keyword \nothing
//@requires: preconditions of method — see JML conditions syntax
//@ensures: postconditions of method — see JML conditions syntax
//@signals: describes an exception that the method could throw and the conditions on which it happens — see JML conditions syntax
//@pure: declares that the method is an observer, meaning that does not change any values of the class variables. Note: pure methods are implicitly //@assignable: \nothing
//@also: the method inherits specifications from its supertypes

Invariants

Invariants specify conditions that are satisfied at the beginning and end of any method invocation and at the end of constructor invocation.

An invariant can be public or private, depending on which type of variables and methods it uses (only public => public invariant; at least one private => private invariant).

Important Notice: Invariants do not have to hold during the execution of a method but they can temporally be broken.

Typical Abstract Object

It is used when the structure of the class is not enough to describe entirely the pre/post conditions and it is needed a backup object that helps to describe in JML everything is needed. This object must be described in //@spec_public .

3. JML conditions syntax

JML conditions are the conditions needed into the //@requires , //@ensures and //@invariant statements.

Conditions are written in Hoare logic (the commonly known logic) and must always be able to return a boolean (true/false).

Java methods like .equals() , .containsAll() , .subList(), etc can be used to enrich the conditions.

If a condition is too much complex to be formalized, human-language can be used; in that case the JML Program Verification Tool will always mark it as “satisfied” . This fact makes usage of human-language into JML conditions quite useless. The only good usage is in order to achieve better comprehension between who writes the pre/post conditions and who actually implements the code.

JML syntax provides also special quantifiers and operators:

Quantifiers

\forall variable; condition; statement means that for all values of “variable” that soddisfy the “condition”, “statement” is true.
\exists variable; range; statement return true if exists at least one value for “variable” into the “range” (optional) that makes true the “statement”. On the contrary, returns false.
\numof variable; condition returns the number of times “variable” satisfy “condition”
condition ? if_true : if_false generally known as ternary operator, it can be used also in JML statements

Note: “condition” and “statement” follow the “JML conditions syntax” explained in the previous paragraph.

Operators

\result is the value returned by the method it’s being described
\old(statement) the statement inside the brackets uses the old variables, meaning that uses the variables’ values as they were before method execution
\sum,\product,\result ,\result …work in progress…