在埃菲爾比較對象/值而不是參考

Question

我一直在試圖弄清楚如何使下列代碼的後置工作。 有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功能時，它只是使結果爲false。 任何幫助非常感謝:)

Answer 1

我假設從您的代碼中，客戶和old_customers是CONTAINER（ARRAY，LIST，STACK，QUEUE等）的後裔類型然後，您可以使用customers.compare_objects（或old_customers。 compare_objects）要求容器在搜索時使用is_equal而不是「=」。