Является ли Java-модельный язык исполняемым?

Я изучаю курс разработки программного обеспечения, и там я видел использование JML. Вот пример кода:Является ли Java-модельный язык исполняемым?

//@ requires f >= 0.0 
public float sqrt(float f) { 
    return f/2; 
}

В нем говорится, что формальные спецификации JML являются исполняемыми!

Мой вопрос: когда мы называем эту функцию sqrt с f = -4, этот код дает ошибку или генерирует исключение или дает какие-либо предупреждения? Я попробовал это на своем компьютере, он просто хорошо работал и распечатывал -2. Тогда что означает, что JML являются исполняемыми? Почему мы не используем только комментарии для этого? Может ли кто-нибудь объяснить?

Благодаря

источник

2013-05-28 yrazlik

Ну, вот код, и я спрашиваю кое-что о коде. Я не понимаю нисходящего! – yrazlik

JML не является частью Java. Это расширение, разработанное коалицией исследователей, но без официального одобрения. Таким образом, JML-аннотации не учитываются компилятором Java, но вы можете скомпилировать JML-аннотированную Java-программу со специальным компилятором, чтобы учитывались исполняемые спецификации. Например, JML4C.

источник

2013-05-28 21:43:38

Спасибо, что помогает – yrazlik

Вы не делаете квадратный корень (Math.sqrt(f) см http://docs.oracle.com/javase/6/docs/api/java/lang/Math.html#sqrt(double)), но деление на 2 (f/2). Так что в этом нет ничего плохого. Вам нужно использовать Math.sqrt (...), если это то, что я предполагаю, вам нужно посмотреть имя вашего метода.

источник

2013-05-28 21:37:53

ну на самом деле здесь не важно. Мне просто интересно: я дал предварительное условие функции, заявив, что параметр должен быть> = 0, но я называю его параметром <0, и он работает. Если JML является исполняемым, почему это так? Почему нет ошибок или предупреждений? – yrazlik

О, тогда в этом случае я думаю, что вам не хватает последнего ';' в конце строки. –

Ну, этот код сам по себе не создает никаких предупреждений. Там существует целый ряд инструментов, которые используют Jml спецификации, например:

jmlrac: тест на нарушения утверждений во время выполнения
ESC/Java2: статическая проверка; время компиляции доказательства того, что контракты никогда не нарушаются
jmldoc: документация Javadoc стиль
jmlc: утверждение проверки компилятор
jmlunit: блок тестирования инструмент

В дополнение к этому, JML спецификации, если правильно использовать, выявить намерения программиста для иностранных читателей/сопровождающих кода.

источник

2013-05-28 21:46:19 McMannus

Является ли Java-модельный язык исполняемым?

ответ

Смежные вопросы