Re: loop variant in SPARK ADA

[Jeffrey Carter <spam@spam.com>]

Constantin Porphyrogenete wrote:
> Couldn't find the newsgroup for SPARK.
> Thought I'd try this one.

SPARK discussions have been welcome here in the past. I hope that won't 
be changing soon.

> Read the book. It seems there is no
> way to assert a loop variant to
> help prove termination (I am thinking
> of the Eiffel loop variant).

Presumably you mean a loop invariant?

> Is there any reason SPARK ADA doesn't
> have this?

I don't have the book to hand, but I do have the SPARK Quick Reference 1:

"The _/assert annotation/_ can be used to specify conditions that are to 
be true - of particular use when verifying programs containing loops."

There is then an example of a Div procedure to calculate M/N, giving the 
quotient in Q and the remainder in R. The loop invariant is:

--# assert (M = Q * N + R) and (R >= 0);

-- 
Jeffrey Carter
"Now go away or I shall taunt you a second time."
Monty Python and the Holy Grail
E-mail: jeffrey_r_carter-nr [commercial-at]
         raytheon [period | full stop] com