Проверьте нарушение утверждения в Eiffel, используя Array_List

Класс CUSTOMER

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

часть класса BANK:

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

клиенты относятся к классу CUSTOMER

у банка есть клиенты и у клиентов есть счета

CUSTOMER имеет класс ACCOUNT


eiffel
person geforce    schedule 15.01.2016    source источник

Ответы (2)


arrow_upward
1
arrow_downward

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

  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). Это может занять некоторое время, но в конце концов это окупится. Вы также можете найти полезным раздел о соглашениях об именах в Руководстве по стилю.

person Alexander Kogtenkov    schedule 15.01.2016
comment
Спасибо за помощь, но это не сработало. При размещении оператора create customers.make(10) я получил ошибку компилятора, говорящую о том, что класс, на который я ссылаюсь, отложен. Также при переключении на расширение я все еще получаю ошибку нарушения проверки утверждения. Я сделаю еще один пост, но на этот раз я покажу весь класс CUSTOMER, чтобы понять, почему это вызывает у меня проблемы. - person geforce; 15.01.2016
comment
@GeForce: это означает, что customers имеет тип LIST [CUSTOMER] (отложенный) или аналогичный. В этом случае требуется явное указание типа в инструкции по созданию. Что касается нарушения утверждения для extend - действительно ли оно связано с этим? Это было бы странно, потому что у него есть только одно предварительное условие extendible, которое всегда равно True для ARRAYED_LIST. - person Alexander Kogtenkov; 15.01.2016
comment
Я отредактировал сообщение с классом CUSTOMER. Я добавил ссылку на банк в CUSTOMER и инициализировал его, и некоторые нарушения проверки исчезли, но там все еще есть некоторые нарушения утверждения проверки. Я думаю, что ошибки могут исходить от класса CUSTOMER, потому что я неправильно определил функции или атрибуты. Есть еще некоторые нарушения пост-условия и проверки утверждений, но не каждый тестовый пример, а только 1 или 2. Вы видите что-нибудь еще, что я не добавляю в класс CUSTOMER? - person geforce; 15.01.2016
comment
@GeForce: Если name имеет тот же тип в CUSTOMER и ACCOUNT, я сразу не вижу проблемы. Но как только вы получаете нарушение утверждения, вы можете проверить трассировку исключения или использовать отладчик, чтобы выяснить, что именно пошло не так. - person Alexander Kogtenkov; 16.01.2016

arrow_upward
1
arrow_downward

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

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

person user2783273    schedule 15.01.2016