Проверить Assertion Нарушения в Eiffel с использованием Array_List

Question

класс КЛИЕНТ

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 

часть класса БАНКА:

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 при попытке поставить клиент в массиве. Тег, который я получил, является «valid_index». Я не знаю, почему это неправильно, потому что индекс прав, и я задал счет для массива и дал правильный индекс.

клиенты имеют класса КЛИЕНТА типа

банка клиенты и клиенты имеют счета

КЛИЕНТА имеет СЧЕТ класс

Answer 1

Есть несколько вопросов с представленным кодом.

1. инструкция Создание

   create {ARRAYED_LIST [CUSTOMER]} customers.make (10) 
   

   выделяет достаточно места для хранения 10 элементов. Он также устанавливает customers.count в 0, текущее количество элементов в списке. Нет необходимости сами отслеживать этот номер, используя свой собственный count. Код также предполагает, что признак customers имеет тип ARRAYED_LIST [CUSTOMER]. В этом случае нет причин повторять тип в инструкции создания. Это может быть упрощено до

   create customers.make (10) 
   

2. customers.count обновляется автоматически, когда новые элементы добавляются в список. Его нельзя менять вручную. (И его нельзя изменить, как объяснено в другом ответе.) Чтобы узнать, почему вы нарушаете предварительное условие, вы можете проверить значение customers.count непосредственно перед вызовом customers.put_i_th (в отладчике или путем печати значения на консоли). На данный момент никаких элементов не добавлено, так что это 0.

3. Поскольку ARRAYED_LIST является реализация LIST, пункты должны быть добавлены/удалены с помощью интерфейса LIST (полезно взглянуть на особенности этого класса, включая унаследованные из них). customers.put_i_th может использоваться только для замены существующих элементов (в качестве предварительного условия valid_index предлагает, и комментарий к функции подтверждается: - Заменить i -я запись, если в индексном интервале, на v.).Частности один, что добавляет новый элемент в конец списка extend, поэтому соответствующая строка выглядит

   customers.extend (c) 
   

Общий совет должен был бы обратить внимание на особенность предпосылки и имеют комментарии и посмотреть на интерфейсах классов (имеется соответствующее представление, если вы используете Eiffel IDE). Это может занять некоторое время, но оно окупится в конце. Вы также можете найти раздел о соглашениях об именах в Style Guidelines.

Answer 2

Если посмотреть на особенности `подсчете», вы увидите, что функция , а не атрибут. Он возвращает счет SPECIAL. Затем вы редактируете этот результат. Но если вы посмотрите на {SPECIAL} .count, это встроенная внешняя процедура, а не атрибут. Так что, вероятно, это не вызвано вами. (Вы можете проверить valid_index до вызова put_i_th, чтобы проверить это).

Фундаментальный, ARRAYED_LIST - это СПИСОК, а не ARRAY (это массив, но это деталь реализации). Таким образом, ваш алгоритм недействителен для списка (вы можете добавлять только новые элементы в конец списка с расширением или вперед с помощью put_front. Последнее неэффективно для ARRAYED_LIST.)