January 30th, 2011, 11:32 AM
JML Question [Beginner]
How to define the JML Behaviours for following problem?
In a Sequence (JMLObjectSequence) are objects stored, with different states
example: [0 ... n] //Status "Waiting" , "In Progress", "Complete", "Fail",
jmlsequ.status() = "Waiting";
jmlsequ.status() = "In Progress";
jmlsequ.status() = "Complete";
jmlsequ[n].status() = "Fail";
each element of this sequence has different state
The function delfirstComplete() gives back, a new sequence (= old sequence + first element with status "Complete" is deleted)
example: new_jmlsequ = jmlsequ.DelFirstComplete();
please help, how to define the jml behavirous, especial the ensures?!!
I think to know, how to define the requierements, but i don´t know how to declare that my result is the old without the first Complete job (status = "Complete").
I tried to solve it like this:
/* @ public normal_behaviour
@ requires jmlsequ.isEmpty() == false;
@ requires (\exists int i; jmlsequ.itemAt(i).equals(“Complete”));
@ modifies \jmlsequ;
@ ensures \result == \old(jmlsequ).removeItemAt(i) &&
@ (\exists int i; jmlsequ.itemAt(i).equals(“Complete”) &&
@ (\forall int j; 0 >= j && j < i; !(jmlsequ.itemAt(j).equals(“Complete”) );
If someone knows the answer, pls. help, i thank for your efforts!