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

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

Le Thu, 27 May 2010 23:50:06 +0200, Brian Drummond  
<brian_drummond@btconnect.com> a écrit:
Hi Brian,

> 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)
Yes, sorry, I forget it. In the simple loop case, L is of the same type,  
that is, it is declared as of type T and T'First is equal to 1. So the  
declaration of L in the for-loop and the declaration of L with the simple  
loop, are the same. N is obviously of type T too.

What puzzles me, is that the expression in the Check clause, does not  
depend on any context, it is purely mathematical, thus it should be as  
provable with the simple loop as it is with the for-loop.

I've just done a test a few seconds ago. If I copy the same Check clause  
between the “L := 1;” statement and the begin of the loop, that is:


    L := 1;

    --# check (2 ** (T'Pos (L) + 1)) = ((2 ** T'Pos (L)) * 2);

    loop
       ...
       --# assert ...;
       ...
       --# check (2 ** (T'Pos (L) + 1)) = ((2 ** T'Pos (L)) * 2);
       exit when L = Length;
       L := L + 1;
       ...
    end loop;

then the first occurrence of the Check, at the first location, is proved  
right away by the simplifier, and the second occurrence, is still not  
proved.

Really funny, as the expression does not depends on any context and all  
numbers/expression which appears in, are Universal_Integer [ARM 2005 Annex  
K (175)], so there should be no matter about any range of any kind. Note:  
T'Last is small, it is actually 8.

Will try some others things later. I believe this is an interesting topic  
(unless I did a gentle clumsy thing which I have not already figured).

Have a nice day/night.

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.