Эта статья требует внимания эксперта по данной теме . Июль 2010 г. ) ( |
Язык моделирования Java ( JML ) - это язык спецификации для программ Java , использующий предварительные и постусловия и инварианты стиля Хоара , который следует парадигме проектирования по контракту . Спецификации записываются в виде комментариев Java-аннотаций к исходным файлам, которые, следовательно, могут быть скомпилированы с помощью любого компилятора Java .
Различные инструменты проверки, такие как средство проверки утверждений во время выполнения и средство расширенной статической проверки ( ESC / Java ), помогают в разработке.
Обзор [ править ]
JML - это язык спецификации поведенческого интерфейса для модулей Java. JML предоставляет семантику для формального описания поведения модуля Java, предотвращая неоднозначность намерений разработчиков модуля. JML унаследовал идеи от Эйфеля , Ларча и исчисления уточнений с целью обеспечения строгой формальной семантики, при этом оставаясь доступным для любого 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 для логических and, or и not. Аннотации JML также имеют доступ к объектам Java, методам объектов и операторам, которые находятся в пределах области действия аннотируемого метода и имеют соответствующую видимость. Они объединены, чтобы предоставить формальные спецификации свойств классов, полей и методов. Например, аннотированный пример простого банковского класса может выглядеть так:
public class BankingExample { публичный статический финал int MAX_BALANCE = 1000 ; private / * @ spec_public @ * / int balance ; private / * @ spec_public @ * / логическое isLocked = false ; // @ публичный инвариантный баланс> = 0 && balance <= MAX_BALANCE; // @ назначаемый баланс; // @ обеспечивает баланс == 0; public BankingExample () { это . баланс = 0 ; } // @ требуется 0 <сумма && сумма + баланс <MAX_BALANCE; // @ назначаемый баланс; // @ обеспечивает баланс == \ old (balance) + amount; общественный недействительный кредит ( окончательная сумма int ) { this . баланс + = сумма ; } // @ требуется 0 <сумма && сумма <= баланс; // @ назначаемый баланс; // @ обеспечивает баланс == \ old (balance) - amount; public void debit ( final int amount ) { this . баланс - = сумма ; } // @ гарантирует isLocked == true; public void lockAccount () { this . isLocked = true ; } // @ требуется! isLocked; // @ обеспечивает \ result == баланс; // @ также // @ требуется isLocked; // @ signal_only BankingException; public / * @ pure @ * / int getBalance () выдает исключение BankingException { if ( ! this . isLocked ) { вернуть это . баланс ; } else { выбросить новое исключение BankingException (); } } }
Полная документация по синтаксису JML доступна в Справочном руководстве JML .
Поддержка инструмента [ править ]
Разнообразные инструменты предоставляют функциональные возможности на основе аннотаций JML. Инструменты JML штата Айова предоставляют компилятор проверки утверждений, 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 на файлах Java с аннотациями JML.
- TACO , инструмент анализа программ с открытым исходным кодом, который статически проверяет соответствие программы Java ее спецификации языка моделирования Java.
- Верификатор VerCors
Ссылки [ править ]
- Гэри Т. Ливенс и Юнсик Чеон. Дизайн по контракту с JML ; Черновик учебника.
- Гэри Т. Ливенс , Альберт Л. Бейкер и Клайд Руби. JML: обозначение для детального проектирования ; в Хаим Килов, Бернхард Румпе и Ян Симмондс (редакторы), Поведенческие спецификации предприятий и систем , Kluwer, 1999, глава 12, страницы 175–188.
- Гэри Т. Ливенс , Эрик Полл, Кертис Клифтон, Юнсик Чеон, Клайд Руби, Дэвид Кок, Питер Мюллер, Джозеф Кинири, Патрис Чалин и Дэниел М. Циммерман. Справочное руководство JML (ПРОЕКТ), сентябрь 2009 г. HTML
- Марике Хейсман , Вольфганг Арендт, Даниэль Брунс и Мартин Хентшель. Формальная спецификация с JML . 2014. скачать (CC-BY-NC-ND)
Внешние ссылки [ править ]
- Веб-сайт JML