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

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

Почему это?

Источник

2 ответа

Решение

Перевод SMT (используется как вход для z3) кажется неисправным, когда участвуют двойники. В приведенной ниже программе B, где используются двойные значения вместо целых, константы для вызова или предварительного условия никогда не переводятся в SMT.

Это вина openjmlне z3 - поскольку z3 понадобится что-то в форме (define-fun _JML__tmp3 () Real 2345.0) работать (см. подробный вывод Программы А), но openjml никогда не генерирует это. В общем, поддержка с плавающей запятой кажется глючной.

Программа А (с целочисленными значениями):

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]

Программа Б (с двойными):

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;
            ^
Источник

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

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

Источник
Другие вопросы по тегам