JML：\exists & JMLObjectSequence

Question

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

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

问题是ordersi必须是数组类型，它是JMLObjectSequence.Is类型，有一种方法可以将这个序列转换为数组，语法会是什么样子？

另一种方法是(使用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(){ ...}

这应该是有效的。