JML: \存在 & JML对象序列

Question

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

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

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

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

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

但是 itemAt(i) 返回一个不是 Order 类型的对象 - 因此找不到方法 getStatus() 。

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

Answer 1

怎么样：

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

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

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

这应该是有效的。