我试图有一个结构，他自己谈论变体和Eiffel循环中的不变量，但不理解变体部分！
from
l_array := <<1,2,30,60>>
l_index := l_array.lower
invariant
valid_local_index: l_array.valid_index (l_index) or l_index = l_array.upper + 1
until
l_index > l_array.upper
loop
l_item := l_array.item (l_index)
l_index := l_index + 1
variant
--l_index <= l_array.upper -- will never be false
--l_index -- doesnt work
end
我认为在您的情况下，您希望作为变体的一部分表达的内容类似于以下
l_array.upper - l_index + 1