我正在尝试将 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
这是为什么?
最佳答案
当涉及 double 时,SMT 转换(用作 z3
的输入)似乎有问题。在下面的程序 B 中,它使用 double 而不是整数,调用或前置条件的常量永远不会被翻译成 SMT。
这是 openjml
的错误,而不是 z3
- 因为 z3
需要 (define-fun _JML__tmp3 () Real 2345.0)
可以使用(参见程序 A 的详细输出),但 openjml
永远不会生成它。一般情况下,floating point support seems to be buggy .
程序 A(带整数):
class Test {
//@ requires b > 1234;
void a(int b) { }
void z() { a(2345); }
}
输出(使用 -verbose | grep 234
运行,以搜索详细输出中提及的 1234
或 2345
):
// requires b > 1234;
Pre_1 = b > 1234;
// requires b > 1234;
assume Assignment Pre_1_0_21___4 == b_55 > 1234;
(assert (= BL_58bodyBegin_2 (=> (= _JML___exception_49_49___1 NULL) (=> (= _JML___termination_49_49___2 0) (=> (distinct THIS NULL) (=> (or (= THIS NULL) (and (and (distinct THIS NULL) (javaSubType (javaTypeOf THIS) T_Test)) (jmlSubType (jmlTypeOf THIS) JMLT_Test))) (=> (and (<= (- 2147483648) b_55) (<= b_55 2147483647)) (=> (select _isalloc___0 THIS) (=> (= (select _alloc___0 THIS) 0) (=> (= Pre_1_0_21___3 false) (=> (= Pre_1_0_21___4 (> b_55 1234)) (=> Pre_1_0_21___4 BL_49_AfterLabel_3))))))))))))
a(2345);
// a(2345)
int _JML__tmp3 = 2345;
boolean _JML__tmp6 = _JML__tmp3 > 1234;
// a(2345)
int _JML__tmp3 = 2345
boolean _JML__tmp6 = _JML__tmp3 > 1234
(define-fun _JML__tmp3 () Int 2345)
(define-fun _JML__tmp6 () Bool (> _JML__tmp3 1234))
结果:
EXECUTION
Proof result is unsat
Method checked OK
[total 427ms]
节目 B( double ):
class Test {
//@ requires b > 1234.0;
void a(double b) { }
void z() { a(2345.0); }
}
输出(使用 -verbose | grep 234
运行,以搜索详细输出中提及的 1234.0
或 2345.0
):
// requires b > 1234.0;
Pre_1 = b > 1234.0;
// requires b > 1234.0;
assume Assignment Pre_1_0_29___4 == b_72 > 1234.0;
a(2345.0);
// a(2345.0)
double _JML__tmp3 = 2345.0;
boolean _JML__tmp6 = _JML__tmp3 > 1234.0;
// a(2345.0)
double _JML__tmp3 = 2345.0
boolean _JML__tmp6 = _JML__tmp3 > 1234.0
void z() { a(2345.0); }
//@ requires b > 1234.0;
Test.java:4: a(2345.0)
VALUE: 2345.0 === 0.0
结果:
EXECUTION
Proof result is sat
Some assertion is not valid
Test.java:4: warning: The prover cannot establish an assertion (Precondition: Test.java:2: ) in method z
void z() { a(2345.0); }
^
Test.java:2: warning: Associated declaration: Test.java:4:
//@ requires b > 1234.0;
^
关于java - 关于实数的推理,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/31413679/