JML: \ exists & JMLObjectSequence

Question

im пытается доказать, существует ли объект с определенным статусом в моей коллекции. Моя коллекция состоит из объектов с методом getStatus(). Теперь я хочу доказать, есть ли объект с данным статусом в этой коллекции.

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

Проблема заключается в том, что порядки [I] должны быть типом гайки массива это тип JMLObjectSequence.Is есть способ бросить эту последовательность в массив и как бы синтаксис выглядеть?

Другим способом (с использованием ItemAt (I)):

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

НО ItemAt (я) возвращает объект, который не является типом заказа - поэтому метод GetStatus() Isnt найден.

Я был бы очень рад некоторой помощи. Там много примеров.

Answer 1

Как насчет:

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

Убедитесь, что GetStatus() является нотирован как чистый метод с/@pure/аннотацией, где она определена.

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

Это должно быть действительным.