エッフェルのフィーチャを使用した事後条件違反

Question

これはクラスの一部です。このクラスはBAG [G - > {HASHABLE、COMPARABLE}] と呼ばれ、count、extend、remove、remove_all、add_all ...などの遅延機能を持つADT_BAGから継承し、ドメインを再実装します。 G

のソートされた配列のリストである

ドメイン戻り値Array [G]私は常にオブジェクトの比較とは何かですが、私がチェックし、オブジェクトのためのコードが存在しない事後条件違反「value_semantics」を取得非常に奇妙な比較。

ドメイン機能のコードを何度もリメイクしようとしましたが、それはポストコンディション違反または失敗で終わります。

私はデバッガをチェックすると、「」それはドメインから返される配列は常に0をカウントしているが、私は「」が、カウントはまだ多分0

あるにテーブルからキーを移動するので、これは意味がありません。私は配列にキーを間違って転送していますか？

コード：

count: INTEGER 
     -- cardinality of the domain 
    do 
     result := domain.count -- has to be domain.count because loop invariant: consistent: count = domain.count 
    end 


domain: ARRAY[G] 
     -- sorted domain of bag 
    local 
     tmp: G 
     a: ARRAY[G] 

    do 
     create a.make_empty 

     across 1 |..| (a.count) as i -- MOVING keys from table to array 
      loop 
       across table as t 
        loop 
         if not a.has (t.key) then 
          a.enter (t.key, i.item) 
          i.forth 
         end 
        end 

      end 

     across 1 |..| (a.count-1) as i -- SORTING 
      loop 
       if a[i.item] > a[i.item+1] then 
        tmp := a[i.item] 
        a[i.item] := a[i.item+1] 
        a[i.item+1] := tmp 
       end 

      end 

    Result := a 

    ensure then 
     value_semantics: Result.object_comparison -- VIOLATION THROWN HERE 
     correct_items: across 1 |..| Result.count as j all 
      has(Result[j.item]) end 
     sorted: across 1 |..| (Result.count-1) as j all 
      Result[j.item] <= Result[j.item+1] end 
    end 

テストコード：

 t3: BOOLEAN 
    local 
     sorted_domain: ARRAY[STRING] 
    do 
     comment("t3:test sorted domain") 
     sorted_domain := <<"bolts", "hammers", "nuts">> 
     sorted_domain.compare_objects 
     Result := bag2.domain ~ sorted_domain -- fails here 
     check Result end 
    end 

Answer 1

最初のループacross 1 |..| (a.count) as iはaが空であるため、開始時（要素がない）単一の反復をするつもりされていません。確かに、それはちょうどcreate a.make_emptyで作成されました。

また、テーブル内のキーが一意であるため、結果の配列にキーが追加されているかどうかを確認することはできません。つまり、not a.has (t.key)のテストは常に成功します。

したがって、最初のループはテーブルのキーを移動し、結果の配列に追加する必要があります。この場合、機能{ARRAY}.forceが重要です。新しい要素を追加しても、配列に「穴」はありません。これを実現する1つの方法は、配列の現在の上限の直後に新しい要素を追加することです。

ソートループも正しくありません。ここでは、前のものとは逆の状況になります。ソートは単一のループでは実行できません。少なくとも2つのネストされたループが必要です。テンプレートはの挿入ソートを使用しているようですが、そのアルゴリズムはelsewhereです。

編集：元の回答は{ARRAY}.forceの代わりに{ARRAY}.extendと呼ばれました。残念ながらは一般的に利用できませんが、a.extend (x)はa.force (x, a.upper + 1)と同じ効果があります。