JML: \exists & JMLObjectSequence

Question

im trying to prove if there exists a object with a particular status in my collection. My collection consists of objects with a method called getStatus(). Now i want to prove if there is a object with given status in this collection.

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

The problem is that the orders[i] must be type of array nut it is type of JMLObjectSequence.Is there a way to cast this sequence to an array and how would the syntax look like?

Another way would be (using itemAt(i)):

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

BUT itemAt(i) returns an Object which is not type of Order - so the method getStatus() isnt found.

I would be very glad about some help. There arent much examples out there.

Answer 1

How about:

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

Make sure getStatus() is notated as a pure method with the /@pure/ annotation where it is defined.

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

This should be valid.