Re: loop variant in SPARK ADA

["Constantin Porphyrogenete" <excubiteur@hotmail.com>]

Thanks for the reply.

The reason for my asking was puzzlement over part of a paragraph
in the book on page 72

"Nevertheless, it is all too easy to
forget to think about the problem of termination and
to conclude that a subprogram is correct just because
all the verification conditions are true."

The impression that I got from the book was that the
point of tools like the Examiner and Simplifier was
precisely to prevent this sort of carelessness.

But I guess it is not to difficult to translate a loop variant
into a loop invariant with the help of some extra variables.

Thanks again for the reply.