object - 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(){ ...}

这应该是有效的。