1

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.

Bins Ich
  • 1,822
  • 6
  • 33
  • 47

1 Answers1

2

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.

Andrew
  • 1,608
  • 16
  • 31
  • is there maybe a way to prove that the \result contains the first order in the sequence with the given status? Maybe there are more orders with the same status... – Bins Ich Jan 31 '12 at 09:31