Re: SPARK again : for-loop vs single loop - a strange case

[Phil Thornley <phil.jpthornley@googlemail.com>]

On 27 May, 20:36, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
[...]
> There was a Check clause in the for-loop, which was looking like this:
>
>     for L in T range 1 .. N loop
>        ...
>        --# assert ...;
>        ...
>        --# check (2 ** (T'Pos (L) + 1)) = ((2 ** T'Pos (L)) * 2);
>        ...
>     end loop;
>
> This Check clause was proved by the Simplifier without any trouble.
>
> I then switch to a class loop, looking like this:
>
>     L := 1;
>
>     loop
>        ...
>        --# assert ...;
>        ...
>        --# check (2 ** (T'Pos (L) + 1)) = ((2 ** T'Pos (L)) * 2);
>        exit when L = Length;
>        L := L + 1;
>        ...
>     end loop;
>
> Then, the Simplifier was not able anymore to prove this Check. I don't  
> understand, as this Check should only depends on a basic rule, a rule by  
> definition. So why the same rule is not applied when I use a classic loop  
> instead of a for-loop ?
>
> Does SPARK changes its strategy depending on the structure of the  
> surrounding source so that it may or may not found a match to a rule  
> depending on this context ?

It is difficult to be specific about non-SPARKable code*, but one
difference at the check will be that the upper bound on L has been
lost.

You can get it back by adding L <= Length to the assertion.  [You
might also need to change the test to
exit when L >= Length;]

It is put in there aotomatically for a 'for' loop but not for a simple
loop.

Cheers,

Phil

* If the code is too big to put in a message then you can send it by
email to the address on the proof tutorials and I'll be happy to have
a look at it.