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 определение> @*/

Basic JML syntax provides the following keywords

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:

The Iowa State JML tools provide an assertion checking compiler jmlc which converts JML annotations into runtime assertions, a documentation generator jmldoc which produces Javadoc documentation augmented with extra information from JML annotations, and a unit test generator jmlunit which generates JUnit test code from JML annotations.

• ESC/Java2 [1], an extended static checker which uses JML annotations to perform more rigorous static checking than is otherwise possible.
• OpenJML declares itself the successor of ESC/Java2.
• Daikon, a dynamic invariant generator.
• KeY, which provides an open source theorem prover with a JML front-end and an Eclipse plug-in (JML Editing) with support for syntax highlighting of JML.
• Krakatoa, a static verification tool based on the Why verification platform and using the Coq proof assistant.
• JMLEclipse, a plugin for the Eclipse integrated development environment with support for JML syntax and interfaces to various tools that make use of JML annotations.
• Sireum/Kiasan, a symbolic execution based static analyzer which supports JML as a contract language.
• JMLUnit, a tool to generate files for running JUnit tests on JML annotated Java files.
• TACO, an open source program analysis tool that statically checks the compliance of a Java program against its Java Modeling Language specification.