objectsequenceexistsjml

JML: \exists & JMLObjectSequence

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.

Solution

  • 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.