java - JML が Java の注釈として実装されないのはなぜですか?

Question

C# のコード コントラクトとは対照的に、JML のコード コントラクトは、メソッドのヘッダーでコメントの形式で使用される単なるテキストです。では、アノテーションとして公開した方がよいのではないでしょうか? そうすれば、情報をコンパイルしても、コメントとは対照的に、消去される.classのメタデータに残ります。

何か不足していますか？

Answer 1

私が見る限り、JML は Java アノテーションより何年も前から存在しています。もちろん、おそらく注釈を利用するように更新することもできます。

Answer 2

Java アノテーションを使用した JML の実験的な実装が
あり
ます。