Почему я получил нарушение предварительного условия valid_index в Eiffel?

Я просто тестирую функцию push_at класса контейнера (в основном, созданного массивом). Я не знаю, какая часть моего кода вызывает это нарушение.

push_at (i: INTEGER; s: STRING)

    require
        valid_index: i  >= 1
    do
        container [i] := s

    end

В моем тестере

local
        con: CONTAINER

do
          create {CONTAINER}con.make
          con.push_at (1,"A")
          con.push_at (2,"B")

 Result := con.get(1) ~ "A" and con.get(2) ~ "B"
 check Result end
 end

Спасибо за помощь!


preconditions eiffel
person buzzmind    schedule 22.09.2017    source источник

Ответы (2)


arrow_upward
0
arrow_downward

Это контейнер [i]. Когда вы создадите кон, он будет пуст (возможно, вы не показали нам свой код). Ваше предварительное условие должно отражать предварительное условие для con[]. Что, в свою очередь, должно отражать предварительное условие для {ARRAY}.put, которое вы должны использовать для его реализации. Ваше текущее предварительное условие этого не делает (оно довольно произвольно).

person user2783273    schedule 23.09.2017

arrow_upward
0
arrow_downward

Базовая структура, используемая в качестве хранилища для элементов, не выделяет память для новых элементов автоматически. Некоторые структуры делают это, когда выполняется команда присваивателя container [i] := s. Но это не тот случай в коде, который вы упомянули. Следовательно, индекс i, используемый в этой команде, недействителен, следовательно, нарушение предусловия. Если вы посмотрите на трассировку исключений или стек вызовов, вы увидите, что нарушение предусловия происходит не в функции {CONTAINER}.puch_at, а в {ARRAY}.put или аналогичной, которая — по совпадению и соглашению об именах — использует тот же тег предусловия valid_index.

Существуют разные способы решения проблемы:

  1. Используйте другую структуру для хранения (атрибут container в вашем примере), например. это может быть HASH_TABLE [STRING, INTEGER]. Тогда становится возможным хранить элементы с произвольными индексами.

  2. Убедитесь, что хранилище предварительно выделено. Если вы знаете диапазон возможных индексов, то container можно инициализировать, чтобы использовать их все с самого начала. Его можно создать с помощью create container.make_filled ("", 1, N), где N — максимальный индекс. (Я предполагаю, что container относится к типу ARRAY [STRING].)

  3. Добавляйте элементы один за другим. В этом случае предварительное условие push_at должно проверять, существует ли указанный индекс или находится ли он рядом с ранее выделенным:

    require
      valid_index: i >= 1
      existing_or_adjacent_index:
          container.valid_index (i) or else
          container.valid_index (i - 1)

    Код push_at должен быть адаптирован для использования функции, которая будет выделять новый индекс, если предоставленный выходит за пределы диапазона выделенных индексов:

    container.force (s, i)

Косметика: нет необходимости повторять объявление типа в инструкции создания create {CONTAINER} con.make, потому что тип переменной con равен CONTAINER. Итак, достаточно использовать create con.make.

person Alexander Kogtenkov    schedule 23.09.2017
comment
Спасибо. Я забыл увеличить контейнер. Задача решена. - person buzzmind; 27.09.2017