私はティーチング アシスタントとして、学生が契約により 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。
ここに私のエラーがあります:
$ jmlc RArray.refines-java
parsing RArray.refines-java
parsing RArray1/RArray.java
typechecking RArray1/RArray.java
The .class file 'java/lang/CharSequence.class' appears to be malformed: Bad constant tag: 18
Fatal error - Unable to find a class for java/lang/CharSequence: error: Cannot find type "java.lang.CharSequence"
前に検索しようとしましたが、CLASSPATH が重複しているか、それらの行に何か問題があるようですが、アクセスできませんでした。
この不正なクラスが修正されるかどうかを確認するために、ZIP ファイルを再度ダウンロードしようとしましたが、うまくいきませんでした。
を実行しようとしましjavac RArray.refines-javaたが、想定どおりにコンパイルされるため、jml の問題である必要があります。
の結果は次のjava -versionとおりです。
java version "1.8.0_66"
Java(TM) SE Runtime Environment (build 1.8.0_66-b17)
Java HotSpot(TM) 64-Bit Server VM (build 25.66-b17, mixed mode)
の結果は次のjml -versionとおりです。
Version: Common JML tools release 5.6_rc4 (Mar. 16, 2009)
これを修正する方法について何か考えはありますか？すべてを捨てなくて済むことを願っています。