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 спецификации.