Java Modeling Language

Java Modeling Language (JML) — язык-надстройка над языком программирования Java, позволяющая выполнить формальные описания для модулей, типов и интерфейсов кода Java. В этих описаниях специфицируются допустимые входные, выходные данные, ограничения , исключения, и логика работы описываемого модуля.

Целью данного описания являются:

- создание программ Java согласно парадигме контрактного программирования.
- автодокументирование на базе описаний в JML исходного кода Java.
- автоматическое создание тестов для исходного кода Java. 
- автоматическая проверка кода Java анализаторами кода.

Ограничения языка JML на 2024

Невозможно специфицировать блоки кода Java, которые выполняются параллельно. Описание JML предполагает исключительно последовательное выполнение блоков кода.

Синтакс

JML описания добавляются в код Java в форме комментариев. Это позволяет компилировать/исполнять JML программу любым Java компилятором/интерпретатором. Для отличия строк JML от обычного комментария используют определения, начинающиеся со знака @, например:

 //@ <JML определение>

или

 /*@ <JML определение> @*/

Основные ключевые слова JML:

requires: Defines a precondition on the method that follows.
ensures: Defines a postcondition on the method that follows.
signals: Defines a postcondition for when a given Exception is thrown by the method that follows.
signals_only: Defines what exceptions may be thrown when the given precondition holds.
assignable: Defines which fields are allowed to be assigned to by the method that follows.
pure: Declares a method to be side effect free (like assignable \nothing but can also throw exceptions). Furthermore, a pure method is supposed to always either terminate normally or throw an exception.
invariant: Defines an invariant property of the class.
loop_invariant: Defines a loop invariant for a loop.
also: Combines specification cases and can also declare that a method is inheriting specifications from its supertypes.
assert: Defines a JML assertion.
spec_public: Declares a protected or private variable public for specification purposes.

Basic JML also provides the following expressions

\result: An identifier for the return value of the method that follows.
\old(<expression>): A modifier to refer to the value of the <expression> at the time of entry into a method.
(\forall <decl>; <range-exp>; <body-exp>): The universal quantifier.
(\exists <decl>; <range-exp>; <body-exp>): The existential quantifier.
a ==> b: a implies b
a <== b: a is implied by b
a <==> b: a if and only if b

JML определения могут включать в себя объекты языка Java.

То есть, смысл конкретного определения JML будет зависеть от его местонахождения в коде Java.

Пример программы с использованием JML:

public class BankingExample
{
 
    public static final int MAX_BALANCE = 1000; 
    private /*@ spec_public @*/ int balance;
    private /*@ spec_public @*/ boolean isLocked = false; 
 
    //@ public invariant balance >= 0 && balance <= MAX_BALANCE;
 
    //@ assignable balance;
    //@ ensures balance == 0;
    public BankingExample()
    {
        this.balance = 0;
    }
 
    //@ requires 0 < amount && amount + balance < MAX_BALANCE;
    //@ assignable balance;
    //@ ensures balance == \old(balance) + amount;
    public void credit(final int amount)
    {
        this.balance += amount;
    }
 
    //@ requires 0 < amount && amount <= balance;
    //@ assignable balance;
    //@ ensures balance == \old(balance) - amount;
    public void debit(final int amount)
    {
        this.balance -= amount;
    }
 
    //@ ensures isLocked == true;
    public void lockAccount()
    {
        this.isLocked = true;
    }
 
    //@   requires !isLocked;
    //@   ensures \result == balance;
    //@ also
    //@   requires isLocked;
    //@   signals_only BankingException;
    public /*@ pure @*/ int getBalance() throws BankingException
    {
        if (!this.isLocked)
        {
                return this.balance;
        }
        else
        {
                throw new BankingException();
        }
    }
}

Документация JML актуально на 2024

- сайт разработчиков спецификации
- JML Reference Manual.
- JML Reference Manual(pdf)

Примеры программного обеспечения базирующегося на описаниях JML:

набор утилит от университета США : компилятор jmlc c проверками ограничений накладываемых JML на код Java во время выполнения; автогенератор документации jmldoc ; генератор автотестов модулей jmlunit.
OpenJML инструмент проверки соответствия кода Java его JML спецификации.
Key-Project, сайт исследовательского проекта, разработчики которого создали сервис, на основе которого работают различные расширения для редактора кода Eclipse (есть расширения для формального научного доказательства, что код работает как задумано, расширения для отладчика кода, расширения для создания авто-тестов кода)
JMLUnit, инструмент для генерации файлов; для запуска JUnit тестов; для файлов Java, специфицированных JML.
TACO, открытое программное обеспечение для анализа программ и проверки соответствия кода Java его JML спецификации.