Re: loop variant in SPARK ADA

[Jacob Sparre Andersen <sparre@nbi.dk>]

Constantin Porphyrogenete wrote:

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

I think it is the appropriate newsgroup for SPARK questions, even if
it isn't mentioned explicitly in the charter.

> 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).
>
> Is there any reason SPARK ADA doesn't have this?

I'm tempted to quote Larry Wall on this subject (altough he's talking
about Ada and not SPARK):

  "I remember being impressed with Ada because you could write an
   infinite loop without a faked up condition. The idea being that in
   Ada the typical infinite loop would normally be terminated by
   detonation."

Being more serious; I don't know why the designers of SPARK have made
that decision.

Greetings,

Jacob
-- 
"The point is that I am now a perfectly safe penguin!"