Неизвестные идентификаторы для обеспечения блока в Eiffel - PullRequest
0 голосов
/ 15 сентября 2018

Итак, я новичок в программировании на 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?Большое спасибо заранее!

Ответы [ 2 ]

0 голосов
/ 15 сентября 2018

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

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

  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
    

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

0 голосов
/ 15 сентября 2018

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

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

...