Неизвестные идентификаторы для блока обеспечения в Eiffel

Итак, я новичок в программировании Eiffel и пытаюсь научиться писать постусловия в блоке ensure блока feature, в частности, с циклами записи.

Итак, я попробовал это:

feature
        -- sets the value of a particular in an array to x
    foo (a: ARRAY[INTEGER]; target_val, x: INTEGER)
        require
            valid_target: 1 <= target_val and target_val <= a.count  
        do
            a[target_val] := x
        ensure
            across
                1 |..| a.count as i
            all
                across
                    1 |..| a.count as j
                all
                    i.item /= j.item implies a[i.item] /= a[j.item]
                end
             end
end

Но почему-то получаю неизвестный идентификатор для i и j. Кто-нибудь знает, что вызывает эту ошибку и как я могу ее исправить? Кроме того, есть ли другая альтернатива использованию across ... as ... all ... end в блоке ensure? Большое спасибо заранее!


eiffel post-conditions
person M. Fire    schedule 15.09.2018    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Я не знаю, почему вы получаете ошибку компиляции - я вставил ваш код, и он отлично компилируется.

Между прочим, в правилах стиля Eiffel говорится, что ваш комментарий должен идти ПОСЛЕ имени функции и аргументов, а не перед ними.

person user2783273    schedule 15.09.2018

arrow_upward
1
arrow_downward

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

Есть как минимум несколько альтернатив коду примера:

  1. Замените итерацию по индексам на итерацию по самим структурам:

    across a as u all
    across a as v all
        u.target_index /= v.target_index implies u.item /= v.item
    end
end

  2. Напишите вспомогательную функцию, которая будет выполнять необходимые тесты и возвращать их результаты в виде BOOLEAN.

  3. Добавьте вспомогательную функцию, которая перебирает структуру и принимает тестовый агент в качестве аргумента, подобно

    for_all_with_index (a: ARRAY [BAR]; test: FUNCTION [BAR, INTEGER, BOOLEAN]): BOOLEAN
    do
        Result := across a as c all test (c.item, c.target_index) end
    end

    и передайте агентов, которые будут тестировать предметы. Однако, даже если он хорошо работает с одним агентом, код с вложенными взаимозависимыми агентами становится слишком тяжелым.

person Alexander Kogtenkov    schedule 15.09.2018