Re: loop variant in SPARK ADA

[Georg Bauhaus <bauhaus@futureapps.de>]

Jeffrey Carter wrote:

>> 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?

Eiffel does have both an invariant and a variant in its loop,

from ...
invariant
  invariant_name: cond
variant
  variant_name: int_var   -- expr >= 0, decreasing
until cond
loop
 ...
end loop