eiffel - Eiffel の機能を使用した事後条件違反

Question

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

domain は、G のソートされた配列リストである ARRAY[G] を返します。

オブジェクト比較に関係する事後条件違反「value_semantics」が常に発生しますが、チェックしたところ、オブジェクト比較のコードがありません。これは非常に奇妙です。

ドメイン機能のコードを何度か作り直そうとしましたが、常に事後条件違反または失敗で終わります。

デバッガーをチェックすると、ドメインから返される配列 "a" のカウントは常に 0 ですが、キーをテーブルから "a" に移動してもカウントが 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