java - Razonamiento sobre los reales

z3 openjml

Question

Estoy experimentando con OpenJML en combinación con Z3, y estoy tratando de razonar acerca de los valores de double o float :

class Test {

  //@ requires b > 0;
  void a(double b) {
  }

  void b() {
    a(2.4);
  }
}

Ya descubrí que OpenJML usa AUFLIA como la lógica predeterminada, que no admite datos reals . Ahora estoy usando AUFNIRA .

Desafortunadamente, la herramienta no puede probar esta clase:

→ 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

¿Por qué es esto?

Answer 1

La traducción de SMT (usada como entrada para z3 ) parece estar defectuosa cuando se trata de dobles. En el Programa B a continuación, que utiliza dobles en lugar de ints, las constantes para la llamada o la condición previa nunca se traducen a SMT .

Esto es un error de openjml , no de z3 , ya que z3 necesitaría algo de la forma (define-fun _JML__tmp3 () Real 2345.0) para trabajar (vea la salida detallada del Programa A), pero openjml nunca lo genera. En general, el soporte de punto flotante parece estar defectuoso .

Programa A (con ints):

class Test {
    //@ requires b > 1234;
    void a(int b) { }
    void z() { a(2345); }
}

Salida (ejecutándose con -verbose | grep 234 , para buscar menciones de 1234 o 2345 en la salida detallada):

  // 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))

Resultado:

EXECUTION
Proof result is unsat
Method checked OK
[total 427ms]    

Programa B (con dobles):

class Test {
    //@ requires b > 1234.0;
    void a(double b) { }
    void z() { a(2345.0); }
}

Salida (ejecutando con -verbose | grep 234 , para buscar menciones de 1234.0 o 2345.0 en la salida detallada):

// 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

Resultado:

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

Puede ver en el siguiente enlace, cómo explican cuando una especificación está incompleta. Su caso muestra el mismo comportamiento que el ejemplo en el enlace. Incluso si intenta otros números, fallará porque necesita agregar más cláusulas openjml.

Aquí el enlace: http://soft.vub.ac.be/~qstieven/sq/session8.html