Beetlz - BON - JML check files error (missing postcondition , but postcondition exists)

[atiti]

Here is an example:

jml specification:

/*@ ensures \result ⇐⇒ (e == array[0]

@ e == array[1] @ e == array[2] @ e == array[3] @ e == array[4] @ e == array[5] @ e == array[6] @ e == array[7]); @ pure public static model boolean legal_unit(final int e); @ */

BON Specification:

legal_unit: BOOLEAN → e: INTEGER

require

    e /= Void;

ensure

    Result /= Void; (e = array.item(0) or e = array.item(1) or

        e = array.item(2) or e = array.item(3) or e = array.item(4) or e = array.item(5) or e = array.item(6) or e = array.item(7)) ↔ Result;

end

Check file(s) messages

• legal_unit@MEASUREMENT_UNIT has a surplus postcondition(s): (e = array.item(0) or e = array.item(1) or e = array.item(2) or e = array.item(3) or e = array.item(4) or e = array.item(5) or e = array.item(6) or e = array.item(7)) ↔ Result
• legal_unit@MEASUREMENT_UNIT is missing postcondition: (e = array.item(0) or e = array.item(1) or e = array.item(2) or e = array.item(3) or e = array.item(4) or e = array.item(5) or e = array.item(6) or e = array.item(7)) ↔ Result

Note that : if I have short postcondition as:

legal_ThermSensorType: BOOLEAN → e: INTEGER

require

    e /= Void;

ensure

    Result /= Void; (e = array.item(0) or e = array.item(1)) ↔ Result;

end

Beetlz - BON - JML type checking passed correct.

[atiti]

From: evka (GH: EvkaD) Date: Sun Nov 8 11:29:36 2009

Bug fixed. The tool does recognize the two assertions as equal, if the individual propositions appear in the same order. It will give an error, if they are e.g. \result == 10 || \result == 20 || \result == 30 Result = 30 or Result = 20 or Result = 10 (These details require some sort of theorem prover to be checked correctly.)