Что такое постулирование метода 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; 
    } 
} 

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