1

我一直在试图弄清楚如何使后置条件适用于以下代码。有3个类，Bank是Customer的客户，Customer是Account的客户

这是银行类，我只是不能通过后置条件 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 功能时，它只会使结果为假。任何帮助是极大的赞赏 ：）

4

1 回答 1

1

我从您的代码中推测客户和 old_customers 是 CONTAINER 的后代类型（ARRAY、LIST、STACK、QUEUE 等）。然后您可以使用 customers.compare_objects（或 old_customers.compare_objects）要求 CONTAINER 使用 is_equal 而不是“ =" 搜索时。

于 2016-01-26T02:23:38.737 回答