Re: SPARK : third example for Roesetta - reviewers welcome

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

Le Mon, 16 Aug 2010 06:41:42 +0200, Phil Thornley  
<phil.jpthornley@gmail.com> a écrit:
> It is certainly unusual (I worked on the proofs for a program of
> 150,000 lines and there was just 1 check annotation), and I agree that
> it may put readers off.
If this is that unusual, I am really wrong about SPARK indeed. On the  
other hand, look at the SPARK introduction at WikiPedia, it talks about  
check/assert annotations, no where it talks about user rules. The SPARK  
LRM talks about annotations, no of very few about user rules. Whenever you  
see an introduction about SPARK, it is said to be an Ada subset with  
annotations. And indeed, notations are there.

Do you see the point ?

May there are two very different way to work with SPARK so. This will not  
ease things...

Would be difficult to explain (and to me to) that what is so much focused  
on, just appears in very cases. So why annotations and so much spots on it  
?