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

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

Le Fri, 28 May 2010 10:14:56 +0200, Phil Thornley  
<phil.jpthornley@googlemail.com> a écrit:
> 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.
You're wonderful Phil! This was something near to that: I've added L <=  
Length, it was not OK, so I though if the upper bound hypothesis was lost,  
so as well was probably the one of the lower bound. So I've added L >= 1,  
then figured that the Checked expression was not verified for L lower than  
zero, so thought if one hypothesis was required, this was this only one,  
the one for the lower bound. So I removed the L <= Length and left L >= 1  
only, which was shown to be enough.

Without you, I would not have been able to guess the trouble was there, as  
to me, it was obvious L >= 1, as the type of L, which is really  
Length_Type, has Length_Type'First = 1.

This is still strange in some way, as if I do L >= Length_Type'First, it  
works.

So the Assert clause even drops implicit hypotheses about numeric type  
bounds ? I was thinking this ones were preserved even after an Assert  
clause.

I was pretty sure Assert was still preserving somethings, as I feel I  
remember I have read something suggesting that in one of the Praxis's  
documentation and in yours as well (do not remember which PDF file, and  
there many to check).

> * 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.
Not too big, this was just that as I was afraid my style with SPARK may  
not be good enough to be posted here. I have lot of lines of SPARK proofs  
for few lines of Ada text, which may seems silly to someones... also that  
I like to have explicit things, because it is more easy to understand and  
to track.

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