I was trying to have a structure which talks himself about variants and invariants into Eiffel loops, but don't understand the variant part!
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
I think in your case what you want to express as part of the variant is something like this
l_array.upper - l_index + 1
loop invariant is a property of your loop that you can assert will be true while the loop is executing. The loop variant is a property of your loop that varies as the loop is executed, and will ensure the loop will terminate.
variant is a non negative integer expression and must decrease in each iteration.
lang-eiffelisn't supported yet after I used it. According to <meta.stackexchange.com/questions/184108/…> ("Any language identifiers used in a post that go unrecognized by highlight.js will functionally default to lang-default.") the algorithm will "Guess" the language then. I suspect it's Ada.