comparison - Eiffel で参照の代わりにオブジェクト/値を比較する

Question

次のコードで事後条件を機能させる方法を見つけようとしています。Bank は Customer のクライアント、Customer は Account のクライアントの 3 つのクラスがあります。

これが銀行クラスです。事後条件 other_customer_unchanged を渡すことができません

    new (name1: STRING)
        -- Add a new customer named 'name1'
        -- to the end of list `customers'
    require
        customer_not_already_present:customer_exists(name1)=false

    do
        customers.force (create {CUSTOMER}.make (name1))
        count := customers.count

    ensure
        total_balance_unchanged:
            sum_of_all_balances = old sum_of_all_balances
        num_customers_increased:count /= old count and old count+1=count
        total_unchanged:total = old total
        customer_added_to_list:
            customer_exists (name1)
            and then customers[customer_id (name1)].name ~ name1
            and then customers[customer_id (name1)].balance ~ zero
        other_customers_unchanged:
            customers_unchanged_other_than(name1, old customers.deep_twin)
    end

customers_unchanged_other_thanの特徴はこちら

customers_unchanged_other_than (a_name: STRING;old_customers:like customers): BOOLEAN
        -- Are customers other than `a_name' unchanged?
    local
        c_name: STRING
    do
        from
            Result := true
            customers.start
        until
            customers.after or not Result
        loop
            c_name := customers.item.name
            if c_name /~ a_name then
                Result := Result and then
                    old_customers.has (customers.item)
            end
            customers.forth
        end
    ensure
        Result =
            across
                customers as c
            all
                c.item.name /~ a_name IMPLIES
                    old_customers.has (c.item)
            end
    end

そして、顧客クラスの is_equal 機能を再定義しました

is_equal (other: like Current): BOOLEAN
    do
        Result := name ~ other.name and balance = other.balance
    ensure then
        Result = (name ~ other.name and balance = other.balance)
    end

私は古いcustomer.deep_twinにあるものを調べました.顧客のアイテムが含まれていますが、どういうわけか.has機能を使用すると、Resultがfalseになります. どんな助けでも大歓迎です:)