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

[Brian Drummond <brian_drummond@btconnect.com>]

On Thu, 27 May 2010 21:36:41 +0200, Yannick Duch�ne (Hibou57)
<yannick_duchene@yahoo.fr> wrote:

>Hi all,
>
>This will require some further investigation on my own side, however, I  
>would like to open a topic about it, if ever someone wants to share about  
>the same matter.
>
>I was proving something built around a for-loop. Every thing was going,  
>when I've meet a trouble and decided to switch to a classic loop and an  
>exit statement and a local variable.
>
>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 ?

Is it relevant here that the range of L is known in the first loop, and
can (presumably) be shown to be less than T'Size?

Perhaps L in the second example can be declared of a subtype with
appropriate range? (If it already is, that wasn't shown in the posted
code)

- Brian