java - java PriorityQueue.remove(Object) 方法的后置条件是什么？

Question

我正在研究为 java.util.PriorityQueue.remove(Object object) 方法创建 JML 规范。到目前为止，我已经想到了以下前提：

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

我现在正试图找出后置条件。那么这个方法的 Ensure 字段是什么？我觉得它应该涉及 size() 方法并确保数据不再在队列中，但我不确定如何编写。

Answer 1

这是来自 grepcode 的方法的代码。

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

我会说根据 o 是否存在于队列中，后置条件要么为假要么为真。我不确定这是否是您正在寻找的。