CODEWITHSUNDEEP
eiffelloop-invariant
Eleno
Eleno

Reputation: 3016

Translating Eiffel loops to languages that do not support loop invariants/variants

A loop in Eiffel follows this format: 

from
    Init
invariant
    Invariant
until
    Exit
variant
    Variant
loop
    Body
end

How would you translate the above Eiffel pseudo-code to a language that does not support loop invariants/variants? Let's assume that such target language has an assert instruction to check the invariant/variant.

Upvotes: 0

Views: 168

Answers (1)

Alexander Kogtenkov
Alexander Kogtenkov

Reputation: 5780

It would look like that:

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

Upvotes: 2

Related Questions