Termination without ghost variable

Hello,

if we have a program like this:

while (condition)_Invariant(invariant)_Term(term) {
    body;
}

what happens to the terms 0 <= term <= k and 0 <= term <= k + 1 from the specification? Do they simply become 0 <= term? I don’t see much value in having a termination condition without a bound, although it would still have the potential to strengthen our invariant it would not be able to prove total correctness. In fact it is subsumed by this form:

while (condition)_Invariant(invariant && term) {
    body;
}

Or should we create a new loop bound if none can be found?

You make up a loop bound.

This opens up the question of naming. If I give it a new name there might be a possible collision with names of identifiers in invariant, condition and term. Is there any safe name I can always apply? (Something like loopBound?)

Well, names that can be chosen by the user are not safe.

But since you are already naming variables apart, you might be able to cleverly find a space where the names are guaranteed fresh.

1 Like

Okay, just tested it: The parser rejects variables starting in numbers (e.g. 0x) , so that is a safe space to operate in. The identifier _x is parsed without issue, so that is not safe.

1 Like