Краткий справочник по JML, языку спецификаций Java.

Оглавление

  1. Что такое JML
  2. Заявления JML
  3. Синтаксис условий JML

1. Что такое JML

Язык моделирования Java (JML) - это язык спецификации для Java.

JML следует парадигме программирования по контракту: это означает, что он описывает предварительные / пост-условия кода, которые необходимо соблюдать, чтобы получить правильное и ожидаемое поведение.

Код JML оценивается с помощью инструментов проверки программ JML (самый известный из них OpenJML), которые проверяют, соответствует ли код Java заданным правилам JML. С более формальной точки зрения: оценка JML означает проверку того, не нарушает ли код Java контракт (см. Программирование контракта).

2. Заявления JML

Поскольку JML все еще официально не поддерживается Java, все операторы JML должны быть записаны в комментариях.

Операторы JML всегда относятся к конкретному классу (или методу) Java, поэтому они должны быть записаны внутри скобок основного класса. Когда они относятся к конкретному методу, они должны быть записаны внутри скобок метода сразу под объявлением (перед объявлением переменных и методов).

Общие инструкции JML

  • //@assignable: список переменных (разделенных запятыми), которые могут изменять значение во время выполнения метода (= изменяемые переменные). Если в классе нет изменяемых переменных, используйте зарезервированное ключевое слово \nothing
  • //@requires: предварительные условия метода - см. синтаксис условий JML
  • //@ensures: постусловия метода - см. синтаксис условий JML
  • //@signals: описывает исключение, которое может вызвать метод, и условия, при которых это происходит - см. синтаксис условий JML
  • //@pure: заявляет, что метод является наблюдателем, что означает, что он не изменяет никаких значений переменных класса. Примечание: чистые методы неявно //@assignable: \nothing
  • //@also: метод наследует спецификации от своих супертипов

Инварианты

Инварианты определяют условия, которые выполняются в начале и конце вызова любого метода и в конце вызова конструктора.

Инвариант может быть общедоступным или частным, в зависимости от того, какой тип переменных и методов он использует (только общедоступный = ›общедоступный инвариант; хотя бы один частный =› частный инвариант).

Важное примечание: инварианты не должны сохраняться во время выполнения метода, но они могут быть временно нарушены.

Типичный абстрактный объект

Он используется, когда структуры класса недостаточно для полного описания условий до / после и требуется объект резервной копии, который помогает описать в JML все, что необходимо. Этот объект должен быть описан в //@spec_public.

3. Синтаксис условий JML

Условия JML - это условия, необходимые для операторов //@requires, //@ensures и //@invariant.

Условия записываются с помощью логики Хоара (общеизвестной логики) и всегда должны иметь возможность возвращать логическое значение (истина / ложь).

Методы Java, такие как .equals(), .containsAll(), .subList() и т. д., можно использовать для улучшения условий.

Если условие слишком сложно для формализации, можно использовать человеческий язык ; в этом случае инструмент проверки программы JML всегда будет отмечать его как «удовлетворено». Этот факт делает использование человеческого языка в условиях JML совершенно бесполезным. Единственное хорошее использование - это достижение лучшего понимания между тем, кто пишет предварительные / пост-условия, и тем, кто фактически реализует код.

Синтаксис JML также предоставляет специальные квантификаторы и операторы:

Квантификаторы

  • \forall variable; condition; statement означает, что для всех значений «переменной», которые не соответствуют «условию», «утверждение» истинно.
  • \exists variable; range; statement вернуть true, если существует хотя бы одно значение для «переменной» в «диапазоне» (необязательно), которое делает «утверждение» истинным. Напротив, возвращает false.
  • \numof variable; condition возвращает количество раз, когда «переменная» удовлетворяет «условию».
  • condition ? if_true : if_false, обычно известный как тернарный оператор, также может использоваться в операторах JML.

Примечание: «условие» и «оператор» следуют «синтаксису условий JML», описанному в предыдущем абзаце.

Операторы

  • \result - значение , возвращаемое описываемым методом.
  • \old(statement) оператор в скобках использует старые переменные, то есть использует значения переменных, которые были до выполнения метода
  • \sum, \product, \result, \result… в процессе…