☰

JML 错误：.class 文件似乎格式不正确

tag-icon • tag-icon linux java fedora
JML 错误：.class 文件似乎格式不正确

这个问题最初发布于堆栈溢出，我被告知应该将其发布在这里。

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

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

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

然而，为了做到这一点，他们必须在学校的电脑上安装 JML，显然没有人有 root 访问权限。我先尝试安装它，看起来它不需要任何 root 访问权限 - 我按照这个法语教程， 有了这个压缩文件。

我尝试在我的 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)

您知道如何解决这个问题吗？我希望我不用放弃一切。

答案1

据我所知，JML 仅适用于 Java 1.7

尝试将您的项目更改为 java 1.7，看看它是否有效。另外检查您的编译器是否不是高于 JML 支持的版本。

以下是一些信息:[1]:http://jmlspecs.sourceforge.net/

@编辑

我在 Eclipse 中使用 JML，我需要选择 Java 7，因为它会自动转到 8。此外，如果您使用终端编译一个简单的类，请在编译时尝试以下命令：$javac -source 1.7 -target 1.7

相关内容