1

コレクションに特定のステータスのオブジェクトが存在するかどうかを証明しようとしています。私のコレクションは、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（）メソッドが見つかりません。

私はいくつかの助けをとてもうれしく思います。そこには多くの例があります。

4

1 に答える 1

2

どうですか：

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

getStatus（）が、定義されている場所に/ @pure /アノテーションが付いた純粋メソッドとして注釈が付けられていることを確認してください。

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

これは有効なはずです。

于 2012-01-31T09:03:10.550 に答える