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

Эта статья включает список ссылок , связанных материалов или внешних ссылок , но ее источники остаются неясными, поскольку в ней отсутствуют встроенные цитаты . Пожалуйста, помогите улучшить эту статью, введя более точные цитаты. ( Апрель 2024 г. ) ( Узнайте, как и когда удалять это сообщение )

Язык моделирования 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>

или

 /*@ <спецификация JML> @*/

Базовый синтаксис 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; //@ назначаемый balance; //@ гарантирует balance == 0; public BankingExample () { this . balance = 0 ; } //@ требует 0 < amount && amount + balance < MAX_BALANCE; //@ назначаемый balance; //@ гарантирует balance == \old(balance) + amount; public void credit ( final int amount ) { this . balance += amount ; } //@ требует 0 < amount && amount <= balance; //@ назначаемый balance; //@ гарантирует balance == \old(balance) - amount; public void debit ( final int amount ) { this . balance -= amount ; } //@ гарантирует isLocked == true; public void lockAccount () { this.isLocked = true ; } //@ требует !isLocked; // @ гарантирует \result == balance; //@ также //@ требует isLocked; // @ signals_only BankingException; public / *@ pure @ */ int getBalance () выдает BankingException { if ( ! this.isLocked ) { return this.balance ; } else { throw new BankingException () ; } } }                                                                                                  

Полная документация по синтаксису JML доступна в Справочном руководстве JML.

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

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

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

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

• веб-сайт JML