Reasoning about reals

Question

I am experimenting with OpenJML in combination with Z3, and I'm trying to reason about double or float values:

class Test {

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

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

I have already found out OpenJML uses AUFLIA as the default logic, which doesn't support reals. I am now using AUFNIRA.

Unfortunately, the tool is unable to prove this class:

→ 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

Why is this?

Beret

Answer 1

The SMT translation (used as input for z3) appears to be faulty when doubles are involved. In Program B below, which uses doubles instead of ints, the constants for either the call or the pre-condition never get translated into SMT.

This is a fault of openjml, not z3 - since z3 would need something of the form (define-fun _JML__tmp3 () Real 2345.0) to work with (see verbose output of Program A), but openjml never generates it. In general, floating point support seems to be buggy.

Program A (with ints):

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

Output (running with -verbose | grep 234, to search for mentions of 1234 or 2345 in the verbose output):

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

Result:

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

Program B (with doubles):

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

Output (running with -verbose | grep 234, to search for mentions of 1234.0 or 2345.0 in the verbose output):

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

Result:

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

Caulfield

Ah, thank you. This gives some insight in what's happening! – Beret

@GhostCat upvoting the original comment (and even better: acting on it) is more than enough :-) – Caulfield

Answer 2

You can see in the following link, how they explain when a specification is incomplete. Your case shows the same behavior than the example in the link. Even if you try other numbers it will fail because you need to add more openjml clauses.

Here the link: http://soft.vub.ac.be/~qstieven/sq/session8.html

Arbitral

Thanks for your answer. In the example in the link however, they are not able to verify the invariant, because they are missing a @requires x >= 0 for the set method. In this case however, it cannot verify that 2.4 > 0, which is odd, and that is my question. – Beret

Maybe because they are different types (Double against int). Can you try //@ requires b > 0.0 ? – Arbitral

The new ideas that I can purpose is to put the //@ requires b > 0; on the function void b() { also make both of them public. – Arbitral