21

Z3 と組み合わせて OpenJML を試しており、次の値について推論しようとしてい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

どうしてこれなの？

4

2 に答える 2

0

次のリンクで、仕様が不完全な場合にどのように説明されているかを確認できます。あなたのケースは、リンクの例と同じ動作を示しています。他の数値を試しても、openjml 句を追加する必要があるため失敗します。

リンクはこちら: http://soft.vub.ac.be/~qstieven/sq/session8.html

于 2015-07-21T13:25:03.150 に答える