問題タブ [jml]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
java - OpenJMLでjmlc、jmlunitを使用するには?
私は Eclipse 用の OpenJML ツール ( http://openjml.org/ ) をインストールして使用していましたが、非常にうまく機能しました。
ただし、コマンド ラインからjmlcおよびjmlunitツールを呼び出す必要があります。インターネットでの検索からわかるように、これらのツールは JML のどこかのディレクトリにあるはずです。これらのツールを PATH に追加し、対応するコマンドを呼び出して通常どおり使用する必要があります。しかし、OpenJML をダウンロードすると、jar ファイルが 3 つしかなく、ディレクトリがまったくありません。また、公式の JML ページには、OpenJML 以外のバージョンをダウンロードするためのリンクはありません。私には明らかな何かが得られないように思えます。
問題は、これらのツールをコマンド ラインで実行する方法を見つける方法です。
前もって感謝します。
java - OpenJML でのプログラムによる静的チェック
OpenJML のマニュアル ( http://jmlspecs.sourceforge.net/OpenJMLUserGuide.pdf ) には、Java コンパイル ユニットの静的チェックをプログラムで実行できることが記載されています。
残念ながら、静的チェック (セクション 5.2.4) のマニュアル エントリは空であり、これに関する具体的な例は示されていないようです。
簡単な例を知っている人はいますか？
jml - 「割り当て可能な a、a[*];」とは 平均？
最近、古い試験で次の JML コードを読みました。
私は理解していません
部。とはa[*]どういう意味ですか? だけだったら何が違うだろう
?
（参照へのリンクは素晴らしいでしょう。）
jml - JMLの「減少」はどのように定義されていますか?
後のステートメントdecreasesは、各ループで厳密に小さくする必要があり、常にゼロ以外でなければなりません。しかし、それは0に達する必要がありますか？1つ小さくする必要がありますか？
java - JML は違反した前提条件をキャッチできません
私のクラス Test には、a という名前の 5 つの int の配列と、選択したセルに 1 を追加するメソッド addOne(int index) があります。メソッドに渡されるインデックスを制御するための単純な前提条件を JML で記述しました。次に、負のインデックスでメソッドを呼び出すこの前提条件に違反しようとしましたが、JML はこのエラーをキャッチできません。どうしたの？
これはテストクラスです:
そして、これはメインです：
それは例外をスローします: java.lang.ArrayIndexOutOfBoundsException: -2.
任意の JML メッセージ。
java - JML エラー : .class ファイルの形式が正しくないようです
私はティーチング アシスタントとして、学生が契約により JML とデザインを学ぶための課題を準備しています。RArray.refines-java (空白の JML アサーションを含む仕様)、 RArray.java (前の仕様を実装するクラス)、およびTestRArray.java (テスト クラス) の3 つのファイルを提供します。
作業を実行するには、次の 3 つのコマンドを計算する必要があります。
jmlc RArray.refines-java(仕様の策定と実装)javac TestRArray.java(テストクラスのコンパイル)jmlrac TestRArray(jml ランタイム アサーション チェッカーによる検証)
ただし、そのためには、学校のコンピューターに JML をインストールする必要があります。学校では、明らかに誰もルート アクセス権を持っていません。最初にインストールしようとしましたが、ルート アクセスは必要ないようです。このzip ファイルを使用して、このフランス語のチュートリアルに従いました。
ubuntu 14.04ラップトップで試してみましたが、問題なく動作し、割り当ての結果を管理できました。学校でも、Fedora では、問題なくツールをインストールして、PATH に追加できます。しかし、学校で を実行するとエラーが発生します
jmlc RArray.refines-java。
ここに私のエラーがあります:
前に検索しようとしましたが、CLASSPATH が重複しているか、それらの行に何か問題があるようですが、アクセスできませんでした。
この不正なクラスが修正されるかどうかを確認するために、ZIP ファイルを再度ダウンロードしようとしましたが、うまくいきませんでした。
を実行しようとしましjavac RArray.refines-javaたが、想定どおりにコンパイルされるため、jml の問題である必要があります。
の結果は次のjava -versionとおりです。
の結果は次のjml -versionとおりです。
これを修正する方法について何か考えはありますか？すべてを捨てなくて済むことを願っています。