JML: \ Существует & 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 - поэтому метод getStatus () не найден.

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

Answer 1

Как насчет:

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

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

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

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