标签: openjml

我正在尝试将OpenJML与Z3结合使用,而我正试图推理double或float重视:

class Test {

  //@ requires b > 0;
  void a(double b) {
  }

  void b() {
    a(2.4);
  }
}

我已经发现OpenJML AUFLIA用作默认逻辑,不支持reals.我现在正在使用AUFNIRA.

不幸的是,该工具无法证明此类:

? java -jar openjml.jar -esc -prover z3_4_3 -exec ./z3 Test.java -noInternalSpecs -logic AUFNIRA

Test.java:8: warning: The prover cannot establish an assertion (Precondition: Test.java:3: ) in method b
    a(2.4);
     ^
Test.java:3: warning: Associated declaration: Test.java:8: 
  //@ requires b > 0;
      ^
2 warnings

为什么是这样？