CODEWITHSUNDEEP
language-agnosticlogicverificationvariant
jameshfisher
jameshfisher

Reputation: 36403

Hoare logic: how does a strictly decreasing loop variant by itself prove termination?

Referring to the while rule for total correctness, WP seems to tell me that just finding a loop variant that strictly decreases is enough to prove termination. I can't accept that, either because I'm missing something or the rule is wrong. Consider

int i = 1000;
while(true) i--;

in which the value of variable i is a strictly decreasing loop variant, but the loop certainly doesn't terminate.

Surely the rule needs to have an additional precondition, something like i<0 → ¬B (where B is the loop condition in the axiom schema) so that the loop condition eventually 'catches' the loop variant and exits.

Or have I missed something?

Upvotes: 1

Views: 548

Answers (3)

JustinL
JustinL

Reputation: 11

The usual ordering "<" is well-founded on the natural numbers, but not on the integers. In order for a relation to be well-founded, every non-empty subset of its domain must have a minimal element. Since it can be shown that there is no infinite descending chain with respect to a well-founded relation, it follows that a loop with a variant must terminate.

Of course the condition of the loop must be false in the case of a minimal element!

A variant need not be restricted to the natural numbers, however. Transfinite ordinals are also well-ordered.

Upvotes: 1

WReach
WReach

Reputation: 18271

As noted in the Wikipedia article:

[...] the condition B must imply that t is not a minimal element of its range, for otherwise the premise of this rule would be false.

In the case at hand, B is true and t is i. true makes no implication about the minimality of i, so the premise of the rule is not met.

Upvotes: 1

n. m. could be an AI
n. m. could be an AI

Reputation: 119877

The loop-variant must be a natural number. A natural number cannot decrease past zero. Using big words, the loop variant is a value that is monotonically decreasing with respect to a well-founded relation. It's the well-foundedness that's missing from your reasoning.

Upvotes: 5

Related Questions