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