Язык моделирования Java

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

Различные инструменты проверки, такие как средство проверки утверждений во время выполнения и расширенная статическая проверка ( ESC/Java ), помогают в разработке.

Обзор [ править ]

JML — это язык спецификации поведенческого интерфейса для модулей Java. JML предоставляет семантику для формального описания поведения модуля Java, предотвращая двусмысленность в отношении намерений разработчиков модуля. JML унаследовал идеи от Eiffel , Larch и Refinement Calculus , с целью обеспечить строгую формальную семантику, оставаясь при этом доступным для любого Java-программиста. Доступны различные инструменты, использующие поведенческие спецификации JML. Поскольку спецификации могут быть записаны в виде аннотаций в программных файлах Java или сохранены в отдельных файлах спецификаций, модули Java со спецификациями JML можно компилировать без изменений с помощью любого компилятора Java.

Синтаксис [ править ]

Спецификации JML добавляются в код Java в виде аннотаций в комментариях. Комментарии Java интерпретируются как аннотации JML, если они начинаются со знака @. То есть комментарии вида

 //@ <JML specification>

или

 /*@ <JML specification> @*/

Базовый синтаксис JML предоставляет следующие ключевые слова

requires: Определяет предварительное условие для метода . следующего
ensures: Определяет постусловие для следующего метода.
signals: Определяет постусловие, когда данное исключение генерируется следующим методом.
signals_only: Определяет, какие исключения могут быть выданы при выполнении данного предварительного условия.
assignable: Определяет, каким полям разрешено назначать следующий метод.
pure: Объявляет метод без побочных эффектов (например, assignable \nothing но также может генерировать исключения). Более того, предполагается, что чистый метод всегда либо завершается нормально, либо генерирует исключение.
invariant: Определяет инвариантное свойство класса .
loop_invariant: Определяет инвариант цикла для цикла.
also: Объединяет случаи спецификации, а также может объявить, что метод наследует спецификации от своих супертипов.
assert: JML Определяет утверждение .
spec_public: Объявляет защищенную или частную переменную общедоступной для целей спецификации.

Базовый JML также предоставляет следующие выражения

\result: Идентификатор возвращаемого значения следующего метода.
\old(<expression>): Модификатор для ссылки на значение <expression> во время входа в метод.
(\forall <decl>; <range-exp>; <body-exp>): Универсальный квантификатор .
(\exists <decl>; <range-exp>; <body-exp>): Экзистенциальный квантор .
a ==> b: a подразумевает b
a <== b: a подразумевается b
a <==> b: a тогда и только тогда, когда b

а также стандартный синтаксис Java для логических и, или, и нет. Аннотации JML также имеют доступ к объектам Java, методам объектов и операторам, которые находятся в области действия аннотируемого метода и имеют соответствующую видимость. Они объединены для предоставления формальных спецификаций свойств классов, полей и методов. Например, аннотированный пример простого банковского класса может выглядеть так:

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 доступна в Справочном руководстве JML .

Поддержка инструментов [ править ]

Различные инструменты предоставляют функциональные возможности, основанные на аннотациях JML. Инструменты JML штата Айова предоставляют компилятор проверки утверждений. jmlc который преобразует аннотации JML в утверждения времени выполнения, генератор документации jmldoc который создает документацию Javadoc , дополненную дополнительной информацией из аннотаций JML, и генератор модульных тестов. jmlunit который генерирует тестовый код JUnit из аннотаций JML.

Независимые группы работают над инструментами, использующими аннотации JML. К ним относятся:

ESC/Java2 [1] — расширенная статическая проверка, которая использует аннотации JML для выполнения более строгой статической проверки, чем это возможно в противном случае.
OpenJML объявляет себя преемником ESC/Java2.
Daikon — динамический инвариантный генератор.
KeY , который предоставляет средство доказательства теорем с открытым исходным кодом с интерфейсом JML и модулем Eclipse подключаемым ( JML Editing ) с поддержкой подсветки синтаксиса JML.
Krakatoa — инструмент статической проверки, основанный на платформе проверки «Почему» и использующий помощника проверки Coq .
JMLEclipse — плагин для интегрированной среды разработки Eclipse с поддержкой синтаксиса JML и интерфейсами для различных инструментов, использующих аннотации JML.
Sireum/Kiasan — статический анализатор на основе символьного выполнения, который поддерживает JML в качестве языка контрактов.
JMLUnit — инструмент для создания файлов для запуска тестов JUnit для файлов Java с аннотациями JML.
TACO , инструмент анализа программ с открытым исходным кодом, который статически проверяет соответствие программы Java спецификации языка моделирования Java.

Ссылки [ править ]

Гэри Т. Ливенс и Юнсик Чон. Проектирование по контракту с JML ; Проект учебника.
Гэри Т. Ливенс , Альберт Л. Бейкер и Клайд Руби. JML: обозначения для детального проектирования ; в Хаим Килов, Бернхард Румпе и Ян Симмондс (редакторы), Поведенческие характеристики бизнеса и систем , Kluwer, 1999, глава 12, страницы 175-188.
Гэри Т. Ливенс , Эрик Полл, Кертис Клифтон, Юнсик Чеон, Клайд Руби, Дэвид Кок, Питер Мюллер, Джозеф Кинири, Патрис Чалин и Дэниел М. Циммерман. Справочное руководство JML (ПРОЕКТ), сентябрь 2009 г. HTML.
Марике Хейсман , Вольфганг Арендт, Даниэль Брунс и Мартин Хентшель. Формальная спецификация с JML . 2014. скачать (CC-BY-NC-ND)

Внешние ссылки [ править ]

Веб-сайт JML