問題タブ [jml]

Java を使用して単純な msn クライアントを開発していますが、JML ライブラリを使用して http プロキシ パラメータを設定する方法がわかりません。どうやらそれはライブラリでネイティブではありません=/

JML を使用していくつかの単純なクラスをテストしています。クラス Interval.java 、 SequenceInterval.java 、および TestSequence.java がすべて同じパッケージ(デフォルト パッケージ)に含まれています。jmlc を使用して SequenceInterval をコンパイルしようとすると、同じエラーが表示されます。

すべての行で、タイプ Interval のオブジェクトを使用します。ESCJava と JML を使用するのは初めてなので、まったくの初心者です。私はちょっと忘れましたか？「モデルのインポート」アノテーションについて読みましたが、Java コードでクラス Interval を使用しているため、それは必要ありません。では、どうすればこのエラーを取り除くことができますか? 明らかにクラスパスの問題ではありません。TNX

JML を読み取ることができる Java で書かれたパーサーを探しています。

基本的に、パーサーが JML ブロックを読み取って、それがどのメソッドに属しているかを認識できるようにしたいと考えています。

OpenJML プロジェクトを見てきましたが、プロジェクトのセットアップだけでは多すぎます。

コレクションに特定のステータスのオブジェクトが存在するかどうかを証明しようとしています。私のコレクションは、getStatus（）というメソッドを持つオブジェクトで構成されています。ここで、このコレクションに特定のステータスのオブジェクトがあるかどうかを証明したいと思います。

問題は、orders [i]が配列ナットの型である必要があることです。これはJMLObjectSequenceの型です。このシーケンスを配列にキャストする方法はありますか？構文はどのようになりますか？

別の方法は（itemAt（i）を使用）です：

ただし、itemAt（i）は、Orderのタイプではないオブジェクトを返すため、getStatus（）メソッドが見つかりません。

私はいくつかの助けをとてもうれしく思います。そこには多くの例があります。

クラス メソッドの JML 事後条件に、別のメソッド呼び出しへの呼び出しを含めることができますか

たとえば、私はこのクラスを持っています:

doB の事後条件については、次のものを使用できensures doA(x) = doA(y)ます。

http://jmlspecs.sourceforge.net/openjml-updatesiteの更新サイトから openJML プラグインをインストールしようとすると、次のエラーが発生します。

以前のバージョンのプラグインをインストールしようとしましたが、すべて同様の「アーティファクトが見つかりません」というエラーが発生します。なぜこれが機能しないのか、誰にも分かりますか？または、Eclipse プラグインを機能させるために使用できる回避策がありますか?

前もって感謝します！

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

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

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

ありがとう

JML をインストールしようとしていて、さまざまな Eclipse ディストリビューションを試した後に成功しましたが、次のエラーが発生します: (eclipse-java-indigo-SR2-win32 を使用) メニューを使用するとエラーが表示されます: JML > 静的チェック (ESC)

証明者の実行可能ファイルが指定されていません - -exec を使用するか、openjml.prover を定義して ください。

画像リンク

クラスがありEdge.javaます。OpenJML で実行すると、次のようになります。

error: An internal JML error occurred, possibly recoverable. Please report the bug with as much information as you can. Reason: com.sun.tools.javac.code.Symbol$TypeSymbol cannot be cast to com.sun.tools.javac.code.Symbol$ClassSymbol

奇妙なことに、私はまだ jml 表記を入れ始めていません。

私のjdkは1.7で、openjmlは最新です（確認のために両方を再ダウンロードしました）。

これは、openjml を実行するために使用されるコマンドです (サイトの例に従います)。 java -jar "E:\Downloads\openjml\openjml.jar" -esc -prover z3_4_3 -exec "E:\Downloads\z3-4.3.0-x64\bin\z3.exe" -noPurityCheck Test.java

編集:ジェネリックを持つ非常に単純なクラスでさえ、このエラーを引き起こす可能性があることを確認できます:

Edge.java