Loop Variant - Practical Considerations - Why Even Consider A Non-integer Variant?

Why Even Consider A Non-integer Variant?

Why even consider a non-integer or transfinite variant? This question has been raised because in all practical instances where we want to prove that a program terminates, we also want to prove that it terminates in a reasonable amount of time. There are at least two possibilities:

• An upper bound on the number of iterations of a loop may be conditional on proving termination in the first place. It may be desirable to separately (or progressively) prove the three properties of
  • partial correctness,
  • termination, and
  • running time.
• Generality: considering transfinite variants allows all possible proofs of termination for a while loop to be seen in terms of the existence of a variant.