What is the postcondition for the java PriorityQueue.remove(Object) method?

Question

I am looking into creating JML specifications for the java.util.PriorityQueue.remove(Object object) method. So far I have thought of the following precondition:

//@ requires object != null;
//@ requires this.size() > 0;

I am now trying to figure out the postcondition. So what is the ensures field for this method? I feel that it should involve the size() method and making sure that the data is no longer in the queue but I am not sure how to write this.

Answer 1

Here is the code for the method from grepcode.

 public boolean remove(Object o) {
  int i = indexOf(o);
  if (i == -1)
       return false;
  else {
       removeAt(i);
       return true;
  }
}

I would say the postcondition would be either false or true based on whether o is present in the queue or not. I am not sure whether this is what you are looking for.