Инкубатор: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 спецификации.

Категория:Языки программирования по алфавиту Категория:Языки программирования платформы Java Категория:Языки формальных спецификаций Категория:Декларативные языки программирования Категория:Скриптовые языки