Исполняемый язык моделирования Java?

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

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

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

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

Спасибо

Источник

3 ответа

Решение

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

Источник

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

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

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

Источник

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

Источник
Другие вопросы по тегам