Re: GNAT packages in Linux distributions

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

Le Wed, 12 May 2010 10:41:03 +0200, <stefan-lucks@see-the.signature> a  
écrit:
> BTW, SPARK also only provides partial correctness, but no total
> correctness. While SPARK allows to prove that no exception is raised (*),
> it lacks the option to specify (and verify, of course) variants for
> WHILE-loops (**). Eiffel supports such
> invariants.
>
> [...]
>
> (**) I just read that the most recent version of SPARK is able to deal
>      with generics. Great! Maybe, SPARK has also recently learned how to
>      specify and prove loop variants?
At the end of [Praxis SPARK 95 4.5] you may read the following :


> It is also guaranteed that code is “reducible”, i.e. that
> every loop has a single entry point, simplifying the
> generation of verification conditions from loop invariants.

So there are some proofs also made on loops at least (still need to learn  
more).

-- 
pragma Asset ? Is that true ? Waaww... great