Транслейтинг Eiffel петли для языков, которые не поддерживают инвариантов цикла/варианты

Question

Петля в Eiffel следующий формат:

from 
    Init 
invariant 
    Invariant 
until 
    Exit 
variant 
    Variant 
loop 
    Body 
end 

Как бы вы перевести выше Эйфелеву псевдо-кода на языке, который не поддерживает инвариантов цикла/варианты? Предположим, что такой целевой язык имеет команду assert для проверки инварианта/варианта.

Answer 1

Это будет выглядеть так:

Init 
last := infinity 
loop 
    assert (Invariant) 
    next := Variant 
    assert (0 <= next and next < last) 
    last := next 
    if Exit then 
     break 
    end 
    Body 
end