Other Language - 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[0].status() = "Waiting";

jmlsequ[1].status() = "In Progress";

jmlsequ[2].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!

thx
Hobby