Войти
Язык моделирования 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 предоставляет следующие ключевые слова
требуетгарантирует, чтоsignalsignal_onlyназначаемыйpureassignable \ nothing, но может также вызывать исключения). Кроме того, чистый метод должен всегда либо завершаться нормально, либо вызывать исключение.invariantloop_invariantтакжеassertspec_publicБазовый JML также предоставляет следующие выражения
\ result\ old () (\ forall ; ; ) (\ exists ; ; ) a ==>baподразумевает, что ba <== baподразумевается ba <==>baтогда и только тогда, когда b, а также стандартный синтаксис Java для логического and, or и not. Аннотации JML также имеют доступ к Java o Объекты, методы и операторы объектов, которые находятся в рамках аннотируемого метода и имеют соответствующую видимость. Они объединены, чтобы предоставить формальные спецификации свойств классов, полей и методов. Например, аннотированный пример простого банковского класса может выглядеть как
public class BankingExample {public static final int MAX_BALANCE = 1000; private / * @ spec_public @ * / int balance; private / * @ spec_public @ * / логическое 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 штата Айова обеспечивают проверку утверждений compiler jmlc, который преобразует аннотации JML в утверждения среды выполнения, генератор документации jmldoc, который создает Javadoc документация дополнена дополнительной информацией из аннотаций JML и генератором модульных тестов jmlunit, который генерирует тестовый код JUnit из аннотаций JML.
Независимые группы работают над инструментами, использующими аннотации JML. К ним относятся:
