带有泛型的 OpenJML？答案

【问题标题】：OpenJML with generics?带有泛型的 OpenJML？
【发布时间】：2014-05-06 08:47:40
【问题描述】：

我有一堂课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

编辑：我可以确认，即使是一个非常简单的泛型类也会导致这个错误：

public class Test<T> {
    T i;
}

Edge.java

public class Edge<K> implements Comparable<Edge<K>> {
    public K n1, n2;
    public int weight;

    public final int tiebreaker;
    public static int nextTiebreaker = 0;

    public Edge(K n1, K n2, int weight) {
        this.n1 = n1;
        this.n2 = n2;
        this.weight = weight;
        tiebreaker = nextTiebreaker++;
    }

    @Override
    public int compareTo(Edge<K> o) {
        if(this.weight > o.weight) return +1;
        if(this.weight < o.weight) return -1;

        return tiebreaker - o.tiebreaker; //Same cost, pick one to be the "larger" 
    }
}

【问题讨论】：

你用的是什么版本的java？（需要是 Java 1.7）。再次尝试下载 OpenJML？（我刚刚在您的 Edge.java 上运行它并且它没有报告任何错误）。你在做比java -jar openjml.jar Edge.java 更复杂的事情吗？如果是这样，请发布命令行。您有可用的 SMT 验证器吗？哪个？
抱歉，我将编辑问题以包含更多信息。
我可以确认我在 Linux 上使用 yices SMT 证明程序得到了相同的异常。

标签： java jml

【解决方案1】：

我发现的解决方法是删除-esc 选项（运行扩展静态检查）。不确定解决此问题的正确方法。

【讨论】：

【解决方案2】：

我也面临类似的问题，但在 temp_release 目录下的 B.java 文件上使用 -esc 选项。

java -jar openjml.jar -noPurityCheck -esc  -progress -exec /Library/bin/z3 -prover z3_4_3 B.java
Proving methods in B
Starting proof of B.B() with prover z3_4_3
error: An internal JML error occurred, possibly recoverable.  Please report the bug with as much information as you can.
  Reason: Unexpected result when querying SMT solver for reason for an unknown result: success
Completed proof of B.B() with prover z3_4_3 - with warnings

B.Java 是

public class B { /*@ invariant true; */ }.

Completed proving methods in B

【讨论】：