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:
> [...]

P.S. Just to tell more, I switched from a for-loop to a classic-loop, so  
as to be able to prove something after the loop, and this was not possible  
with a for-loop, as L is not anymore in the scope after the loop.

I feel classic-loop are probably more handy with proof, due to that it  
leaves some termination states accessible after the loop, and these are  
most likely needed hypothesis to prove many things after a loop.

Or may be I'm wrong ? Do you know a case where a for-loop is better than a  
classic-loop with proofs ?

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