Что является постусловием для метода java PriorityQueue.remove(Object)?

Question

Я смотрю на создание JML-спецификаций для метода java.util.PriorityQueue.remove(Object object). До сих пор я думал о следующем предварительном условии:

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

Я сейчас пытаюсь выяснить постусловие. Так что же такое поле для гарантии для этого метода? Я чувствую, что он должен включать метод size() и убедиться, что данные больше не находятся в очереди, но я не уверен, как это написать.

Answer 1

Вот код для метода из grepcode.

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

Я бы сказал, что постусловие будет либо ложным, либо истинным в зависимости от того, присутствует ли o в очереди или нет. Я не уверен, что это то, что вы ищете.