1

コレクション「col」の最大値を見つけるために、前後の条件を記述しようとしています。再帰的にそれを行う方法がよくわからないので、誰かが助けてくれるかどうか疑問に思っていました!

pre: true 
post: result = ...
4

4 に答える 4

3

post: result= col -> any(a | col->forAll(a2 | a >=a2))

ここで、「any」は条件を満たす要素の 1 つを返します。つまり、select と同様ですが、コレクション内の複数の要素が条件を満たす場合はランダムに選択された単一の要素のみが返されることが保証されます。

「any」内の条件は、選択された要素「a」が他のすべての要素と比較することにより、コレクション内の最大値であることを保証します

このOCLチュートリアルもチェックしてください。実際、集計やその他の種類の統計関数を処理するための OCL の制限は、この言語の未解決の問題の 1 つです。

于 2013-01-04T10:27:09.200 に答える
3

私がすること：

pre:  not col.isEmpty()
post: col -> includes(result) and col -> forAll(a | a <= result)

EDIT2: この質問について、OCL の専門家と話し合いました。col -> includes(result)彼らは、ポスト状態にする必要があると指摘しました。それ以外の場合resultは、 のすべての要素よりも大きい任意の値にすることができますがcol、必ずしも の要素であるとは限りませんcol。

編集：

事後条件の意味: の各要素aについて、 The operation is defined on page 45 of the OCL Specification 2.3.1colが true です。その構文はa <= resultforAll

collection->forAll( v | boolean-expression-with-v )

そのセマンティクスは次のとおりです。

この forAll 式はブール値になります。コレクションのすべての要素に対して boolean-expression が true の場合、結果は true です。コレクション内の 1 つ以上の v に対して boolean-expression-with-v が false である場合、式全体が false と評価されます。たとえば、会社のコンテキストでは次のようになります。

例:

 context Company
      inv: self.employee->forAll( age <= 65 )
      inv: self.employee->forAll( p | p.age <= 65 )
      inv: self.employee->forAll( p : Person | p.age <= 65 )
于 2013-01-04T08:41:40.983 に答える
1

OCL は次のように定義Collection::max()します。

post: result = self->iterate( elem; acc : T = self.first() | acc.max(elem) )

ここで、「要素によってサポートされる最大操作は、型 T の 1 つのパラメーターを取り、結合的かつ可換的でなければなりません」 .

は post: result = self->iterate( elem; acc : T = self.asSequence()->first() | acc.max(elem) )first()に対して定義されていないため、次のようにする必要があることを理解していCollectionます。

コレクションはシーケンスに変換されます。アキュムレータ ( acc) は、シーケンスの最初の値で初期化されます。acciterate 式は、現在の値と iteratorの間の最大値としてアキュムレータを更新しますelem。コレクションが空の場合、結果はself.first()になります。これはinvalidです。

于 2013-02-28T18:37:02.807 に答える
0

私があなたを正しく理解していれば、これが役立つかもしれません: http://math.hws.edu/eck/cs124/javanotes6/c4/s6.html#subroutines.6.1

前提条件は、メソッドが実行される前に満たさなければならないものです。これは主に、コレクションが null ではないなど、入力データに関するいくつかのアサートになります。事後条件は、メソッドが終了した後に何が true になるかを定義します。あなたの場合、これはたとえば次のようになります。メソッドは、指定されたコレクションの値の最大値を持つ要素を返しました。

于 2013-01-03T20:49:09.230 に答える