Введение

Язык спецификации для программ Java

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

Обзор

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

Поддержка инструмента

Различные инструменты предоставляют функциональность, основанную на аннотациях JML. Инструменты JML, разработанные в штате Айова, включают компилятор для проверки утверждений jmlc, который преобразует аннотации JML в runtime assertions, генератор документации jmldoc, создающий документацию Javadoc, дополненную информацией из аннотаций JML, и генератор модульных тестов jmlunit, генерирующий код тестов JUnit на основе аннотаций JML. Независимые группы разрабатывают инструменты, использующие аннотации JML. К ним относятся: ESC/Java2, расширенный статический анализатор, использующий аннотации JML для более строгой статической проверки, чем обычно возможно. OpenJML позиционирует себя как преемника ESC/Java2. Daikon, генератор динамических инвариантов. KeY, предоставляющий средство доказательства теорем с открытым исходным кодом с JML-интерфейсом и плагин для Eclipse (JML Editing) с поддержкой подсветки синтаксиса JML. Krakatoa, инструмент статической верификации, основанный на платформе верификации Why и использующий систему доказательств Coq. JMLEclipse, плагин для интегрированной среды разработки Eclipse с поддержкой синтаксиса JML и интерфейсами к различным инструментам, использующим аннотации JML. Sireum/Kiasan, статический анализатор, основанный на символьном выполнении, поддерживающий JML как язык спецификаций. JMLUnit, инструмент для генерации файлов для запуска модульных тестов JUnit для Java-файлов, аннотированных JML. TACO, инструмент статического анализа программ с открытым исходным кодом, проверяющий соответствие Java-программы её спецификации на языке моделирования Java.