Я экспериментирую с 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
Почему это?