Issues in both ESC and RAC for quantified expressions

[itlchriss]

Hi David,

I am working on a topic of using quantified expressions in verification. In order to use JML, OpenJML has caught my attention. However, I found that there are weird cases in using quantified expressions. First of all, I provide my expressions below,

/*@ensures (\exists boolean x1; x1 == \result; \exists boolean z1; z1 == true; x1 == z1)
            ==>
            (\exists int x2; x2 == number; \exists int z2; (z2 % 2 == 0); x2 == z2);
@*/
/*@ensures (\exists boolean x1; x1 == \result; \exists boolean z1; z1 == false; x1 == z1)
            ==>
            (\exists int x2; x2 == number; \exists int z2; !(z2 % 2 == 0); x2 == z2);
@*/

1. I found these cases are not always proved to be correct. I have tried them on Mac, they are always correct for ESC, but not in Ubuntu. I hope there can be a reason.
2. These expressions cannot be used in RAC, the warnings told the current versions may not support the functionality on these expressions. Are there any plan on this :)?
3. Maybe I am wrong, these expressions may have the same meanings as the following, //@ ensures \result == true ==> number %2 == 0; //@ ensures \result == false ==> !(number %2 == 0); Nevertheless, the quantified expressions are not always working, and these later conditions are always worked.

Thanks and Best Regards, Sincerely, Chriss IT. Leong

[davidcok]

A few comments:

• anything using % requires non-linear arithmetic, which will heavily stress the SMT solver
• a quantified (\exists int x; ... ) is not supported because of the general necessity of iterating over all int's (which, though finite, is a lot). A constrained range is allowed. Arguably we should allow you case above where the range is just a single element.
• the success of proving quantified expressions in ESC, is up to the underlying SMT solver. It is curious that there is a difference between Linux and Mac. They both do use version 4.3.1, but there may be slight differences in search behavior on different platforms. Just speculation.