JML：\ exists＆JMLObjectSequence

Question

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

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

的问题是订单[我]必须阵列螺母的类型是类型JMLObjectSequence.Is的有没有办法这个序列转换为一个数组，以及如何将语法是什么样子？

另一种方法是（用itemAt（I））：

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

BUT itemAt（i）返回一个对象，它是未订购的类型 - 这样的方法的getStatus（）心不是找到。

我很乐意提供一些帮助。那里没有很多例子。

Answer 1

如何：

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

确认的getStatus（）记载为与/ @pure /注释它定义一个纯粹的方法。

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

这应该是有效的。