JML: \exists & JMLObjectSequence

Question

我试图证明我的收藏中是否存在具有特定状态的对象。我的集合由具有称为 getStatus() 的方法的对象组成。现在我想证明这个集合中是否存在具有给定状态的对象。

@ requires (\exists int i; 0 <= i && i < sizeLimit; orders[i].getStatus().equals(Status.New));
public Order getFirstOrder(Status s)

问题是 orders[i] 必须是数组类型，它是 JMLObjectSequence 类型。有没有办法将此序列转换为数组？语法如何？

另一种方法是（使用 itemAt(i)）：

@ requires (\exists int i; 0 <= i && i < sizeLimit; orders.itemAt(i).getStatus().equals(Status.New));

但是 itemAt(i) 返回一个不是 Order 类型的 Object - 所以找不到方法 getStatus()。

如果能得到一些帮助，我会很高兴的。那里没有太多的例子。

Answer 1

怎么样：

((Order)orders.itemAt(i)).getStatus()

确保 getStatus() 在定义时使用 /@pure/ 注释标记为纯方法。

public /*@pure*/ Status getStatus(){ ...}

这应该是有效的。