Using method call in post-condition bug

[atiti]

A method call in Java JML post condition not recognized correctly by Beetlz in BON and therefore Beetlz shows a error marker.

Example: /* JAVA / / protected method in Java that returns a computed value / protected /@ pure @*/ int get_no_of_elected() {...}

/* method in same class that uses protected method in contract */ //@ requires seats >= 0; //@ ensures get_no_of_elected() >= seats; public void setElected(int seats);

--BON-- --feature in the same class in BON get_no_of_elected : INTEGER

set_elected -> seats : INTEGER require seats >= 0; ensure get_no_of_elected >= seats; end

Error tooltip: Multiple markers at this line:

• set_elected@ has a surplus postcondition(s): get_no_of_elected >= seats
• set_elected@ is missing postcondition(s): get_no_of_elected >= seats