eiffel - 将 Eiffel 循环翻译成不支持循环不变量/变量的语言

Question

Eiffel 中的循环遵循以下格式：

from
    Init
invariant
    Invariant
until
    Exit
variant
    Variant
loop
    Body
end

您如何将上述 Eiffel 伪代码翻译成不支持循环不变量/变量的语言？让我们假设这样的目标语言有一个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