4

我是一名助教，为我的学生准备作业，以便他们学习 JML 和合同设计。我给他们 3 个文件：RArray.refines-java（带有空白 JML 断言的规范）、RArray.java（实现先前规范的类）和TestRArray.java（测试类）。

为了执行这项工作，他们必须计算 3 个命令：

  1. jmlc RArray.refines-java（规范和实现的编译）
  2. javac TestRArray.java（测试类的编译）
  3. jmlrac TestRArray（使用 jml 运行时断言检查器进行验证）

然而，为了做到这一点，他们必须在学校的计算机上安装 JML，显然没有人拥有 root 访问权限。我尝试先安装它，它似乎不需要任何 root 访问权限 - 我按照这个法语教程，使用这个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)

您对如何解决此问题有任何想法吗？我希望我不必丢弃所有东西。

4

0 回答 0