loop variant in SPARK ADA

loop variant in SPARK ADA

[Constantin Porphyrogenete]

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

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?

Re: loop variant in SPARK ADA

[Jacob Sparre Andersen]

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!"

Re: loop variant in SPARK ADA

[Jeffrey Carter]

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

Re: loop variant in SPARK ADA

[Georg Bauhaus]

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

Re: loop variant in SPARK ADA

[Jeffrey Carter]

Georg Bauhaus wrote:
> 
> 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

I see. Does this mean you can't write infinite loops in Eiffel?

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

Re: loop variant in SPARK ADA

[Georg Bauhaus]

Jeffrey Carter wrote:
>  Does this mean you can't write infinite loops in Eiffel?

For sure you can write infinite loops, there is no requirement in the
language that force termination. A variant (or an invariant) need not
be given.

    possibly_infinite_loop(eternity: BOOLEAN) is 
        -- one way to write an infinite loop
      do
        from until eternity loop
          do_it_again
        end
      end

Re: loop variant in SPARK ADA

[Rod Chapman]

SPARK doesn't directly support the specificaciton of _variants_
for loops at present.

It's something we've often thought about, but no paying customer
has ever asked us for!  We also find that, in most embedded, critical
systems, the loop structures used are so simple that establishing
their termination is hardly ever a big problem.

- Rod Chapman, SPARK Team, Praxis

Re: loop variant in SPARK ADA

[Constantin Porphyrogenete]

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.

Re: loop variant in SPARK ADA

[Jeffrey Carter]

Constantin Porphyrogenete wrote:
> 
> "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."

I suspect this refers to the general concept of correctness proofs. The 
correctness proofs in SPARK are technically incomplete proofs because 
they don't prove termination in general; in other words, they haven't 
solved the halting problem.

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