On Fri, 28 May 2010, Yannick Duch�ne (Hibou57) wrote:

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

A for-loop terminates always. 

A classical loop may run forever. One would prove termination by loop 
variants, but SPARK doesn't support loop variants. (I am sure you know 
that.)

I would consider this a reason to prefer for-loops over classical loops. 

-- 
------ Stefan Lucks   --  Bauhaus-University Weimar  --   Germany  ------
               Stefan dot Lucks at uni minus weimar dot de
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------