1

私はソフトウェア エンジニアリング コースを勉強していますが、そこで JML の使用法を見ました。コードの例を次に示します。

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

正式な JML 仕様が実行可能だということです。

私の質問は、f=-4 でこの sqrt 関数を呼び出すと、このコードはエラーを出すか、例外をスローするか、警告を出すかです。私は自分のコンピューターで試してみましたが、うまく機能し、-2.が出力されました。では、JML が実行可能であるとはどういう意味でしょうか? これを行うためにコメントだけを使用しないのはなぜですか? 誰でも説明できますか？

ありがとう

4

3 に答える 3

1

JML は Java の一部ではありません。これは、研究者の連合によって設計された拡張機能ですが、公式の承認はありません。そのため、JML アノテーションは Java コンパイラーによって考慮されませんが、JML アノテーションが付けられた Java プログラムを特別なコンパイラーでコンパイルして、実行可能な仕様が考慮されるようにすることができます。たとえば、JML4C .

于 2013-05-28T21:43:38.237 に答える