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

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

Le Fri, 28 May 2010 13:50:51 +0200, Phil Thornley  
<phil.jpthornley@googlemail.com> a écrit:
> So the fact that adding L >= Length_Type'First allows the Simplifier
> to prove the check suggests that you are not getting these hypotheses
> - possibly for one of the above reasons.
OK, with the for-loop, L cannot goes outside of the range expression, so  
the Examiner can always assume these hypotheses exist. However, there is  
still the Length_Type and associated VC for RTC, which can turn into  
hypotheses. I would understand I may had a trouble with a VC associated to  
a RTC, I can't understand this one.

You suggested to look Generation of RTC, section 4.5.2.1.

It says:
> The default assertion states the subprogram’s precondition
> is satisfied
OK.

Then
> In the case of for loops, the invariant also states that theloop counter  
> is in its subtype.
OK.

I could not see something about local variables here indeed.

Something about it is said in 4.2:
> Additionally, the Examiner exploits the benefit of data
> flow analysis by assuming that a local variable, anywhereit is  
> referenced in an expression, must be validly in type.
providing there is no flow error, as explained later in 4.2

There was no flow error, so the Length_Type range should be enough as an  
hypothesis, and it should be there (and that was my assumption, that is  
why I did not understood what's happened).


> If you should be getting these hypotheses then post (or email) the
> complete SPARKable code.
Will see. I will try somethings else before.

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