Рассуждения о реалов

Question

Я экспериментировал с 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 

Почему это?

Answer 1

СМТ перевод (используется в качестве входных данных для z3) оказывается дефектным, когда двойники участвуют. В Программе B ниже, в которой вместо ints используются удвоения, константы для вызова или предварительного условия никогда не переводится в 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); } 
} 

Output (бег с -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 (с двойниками):

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; 
      ^

Answer 2

Вы можете увидеть в следующей ссылке, как они объясняют, когда спецификация неполна. Ваш случай показывает то же поведение, что и пример в ссылке. Даже если вы попробуете другие номера, это не сработает, потому что вам нужно добавить дополнительные предложения openjml.

Вот ссылка: http://soft.vub.ac.be/~qstieven/sq/session8.html