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

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

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 ?

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 ?

I've checked multiple times, this does not seems to be an error, it do the  
same each time I switch from one to the other.