Язык моделирования Java
-
Обзор JML
- JML — это язык спецификаций для Java, использующий предварительные и постусловия.
- Спецификации записываются в виде аннотаций к исходным файлам Java.
- Инструменты проверки, такие как ESC/Java, помогают в разработке.
-
Синтаксис и инструментальная поддержка
- Спецификации JML добавляются в код в виде аннотаций.
- Базовый синтаксис включает ключевые слова и выражения.
- Аннотации JML имеют доступ к объектам Java.
- Различные инструменты, такие как jmlc, jmldoc и jmlunit, используют аннотации JML.
-
Инструментальная поддержка и рекомендации
- Инструменты JML включают компилятор, генератор документации и генератор модульных тестов.
- Существуют независимые инструменты, такие как ESC/Java2 и OpenJML.
- JMLUnit используется для создания тестовых файлов JUnit.
- TACO — это инструмент для статической проверки соответствия Java-программы спецификации JML.
-
Ссылки и ресурсы
- Веб-сайт JML предоставляет дополнительную информацию и ссылки на инструменты.
- Существуют официальные руководства и спецификации JML.