README.md

示例:abs —— OpenJML -esc 的真实闭环

和 examples/abs-int/(C/ACSL)几乎是同一个 bug,换成 Java + JML,验证 ../../references/java-openjml.md 里的结论和命令是否准确。

文件

• AbsBuggy.java —— 有 bug 的版本
• AbsFixed.java —— 修复后的版本

代码(buggy)

public class AbsBuggy {
    //@ ensures \result >= 0;
    public static int abs(int x) {
        if (x < 0) return -x;
        return x;
    }
}

requires 没有排除 x == Integer.MIN_VALUE,这个输入下 -x 会整数溢出(在 Java 里,Integer.MIN_VALUE 取负数学上应为 2147483648,超出 int 范围,实际回绕仍是 Integer.MIN_VALUE,是负数,违反 \result >= 0)。

第一步:OpenJML 实测(有 bug 的版本)

openjml -esc AbsBuggy.java

实测输出:

AbsBuggy.java:4: verify: The prover cannot establish an assertion (ArithmeticOperationRange) in method abs: int negation
        if (x < 0) return -x;
                          ^
AbsBuggy.java:4: verify: The prover cannot establish an assertion (Postcondition: AbsBuggy.java:2:) in method abs
        if (x < 0) return -x;
                   ^
3 verification failures

两处失败:int negation 的溢出检查,以及由此导致的 ensures \result >= 0 后置条件证明失败——和 C/ACSL 那边 typed_abs_int_assert_rte_signed_overflow 证不出来是同一类问题。

第二步:修复

public class AbsFixed {
    //@ requires x > Integer.MIN_VALUE;
    //@ ensures \result >= 0;
    public static int abs(int x) {
        if (x < 0) return -x;
        return x;
    }
}

第三步:OpenJML 确认修复(实测)

openjml -esc AbsFixed.java

实测输出:无(退出码 0)——全部验证通过。