使用 Array_List 检查 Eiffel 中的断言违规

Question

客户class

class
    CUSTOMER
create
    make

feature{NONE} -- Creation

make(a_name:STRING)
        -- Create a customer with an `account'
    local
        l_account: ACCOUNT
        l_name: IMMUTABLE_STRING_8
        l_bank: BANK
    do
        l_name := a_name
        name := l_name
        create l_account.make_with_name (a_name)
        create l_bank.make
        b := l_bank
        account := l_account
    ensure
        correct_name: name ~ a_name
        correct_balance: balance = balance.zero
    end

feature -- queries

name: IMMUTABLE_STRING_8

balance: VALUE
    do
        Result := account.balance
    end

account: ACCOUNT

b: BANK




 invariant
    name_consistency: name ~ account.name
    balance_consistency: balance = account.balance
 end

部分银行class:

   make  -- make a bank

       do
          count := 0
          create [ARRAY_LIST][CUSTOMER] customers.make(10)
          customers.count.set_Item(10)

       end

   new(name1: STRING) -- add a new customer to bank

       require 
         ....
       local
            c: CUSTOMER
       do
          create c.make(name1)
          customers.extend(c)
          count := count + 1




       ensure
          ...
       end

我在尝试将客户放入数组时从 ARRAY_LIST class 收到检查断言错误。我得到的标签是 "valid_index" 我不知道为什么它是错误的，因为索引是正确的，我设置了数组的计数并给出了正确的索引。

客户的类型为 CUSTOMER class

银行有客户，客户有账户

客户有一个帐户class

Answer 1

如果您查看功能“count”，您会发现它是一个函数，而不是一个属性。它 returns SPECIAL 的计数。然后编辑此结果。但是，如果您查看 {SPECIAL}.count，它是一个 built-in 外部例程，而不是属性。所以它可能不受你打电话的影响。（您可以在调用 put_i_th 之前测试 valid_index 来验证这一点）。

从根本上说，ARRAYED_LIST 是一个 LIST，而不是一个 ARRAY（它是一个 ARRAY，但这是一个实现细节）。因此，您的算法对于列表无效（您只能使用扩展将新项目添加到列表的末尾，或者使用 put_front 将新项目添加到列表的前面。后者在 ARRAYED_LIST 上效率低下。）

Answer 2

提供的代码存在一些问题。

创建说明
```
create {ARRAYED_LIST [CUSTOMER]} customers.make (10)
```
分配足够的 space 来存储 10 个元素。它还将 customers.count 设置为 0，即列表中的当前元素数。无需使用您自己的 count 自行跟踪此号码。该代码还建议将属性 customers 声明为 ARRAYED_LIST [CUSTOMER] 类型。在那种情况下，没有理由在创建指令中重复类型。可以简化为
```
create customers.make (10)
```
customers.count 会在新元素添加到列表时自动更新。不应手动更改。（而且它不能像另一个答案中解释的那样改变。）只是为了看看你为什么会违反先决条件，你可以在调用 customers.put_i_th 之前检查 customers.count 的值（在调试器中或通过打印控制台的值）。此时还没有添加任何元素，所以是 0.
因为 ARRAYED_LIST 是 LIST 的实现，项目应该是 added/removed 使用 LIST 的接口（有一个看看这个 class 的特征，包括继承的特征）。 customers.put_i_th 只能用于替换现有元素（如其先决条件 valid_index 所建议和功能注释确认： -- 替换第 i-th 条目，如果在索引间隔中, v.).将新元素添加到列表末尾的特定行是 extend，因此对应的行看起来像
```
customers.extend (c)
```

一般建议是注意功能前提条件和功能注释，并查看 class 界面（如果您使用的是 Eiffel IDE，则有相应的视图）。这可能需要一些时间，但最终会有回报。您可能还会发现 Style Guidelines 中有关命名约定的部分很有用。

使用 Array_List 检查 Eiffel 中的断言违规

Check Assertion Violation in Eiffel using Array_List

eiffel