Re: SPARK

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

Le Thu, 13 May 2010 00:55:02 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> Hope this first question will get a short answer, so let us jump to the  
> second question, which is intended to start with one major deal of SPARK  
> for people who know/use Ada : Ada subset and restrictions (not to  
> disclaim or disagree with, mostly to talk and understand more).

An important quote every one should know about ; especially the last  
sentence:

[Praxis SPARK 95 (5)]
> Some readers may be dismayed to see so many features of Ada removed,
> and feel that SPARK is “too small”. It is by no means the largest
> subset of Ada which would be amenable to analysis by the techniques
> employed in SPADE, but it is significantly larger than SPADE-Pascal,
> which has been found adequate for a substantial number of
> safety-critical projects. The additional features which appear in
> SPARK (such as packages and private types) make programming simpler
> and safer, rather than complicate the verification task. Of course,
> the extent to which Ada must be simplified for high-integrity
> programming will be a matter of opinion: our preoccupation with
> simplicity is based on experience of what can be achieved with a
> high degree of confidence in practice, rather than what can be
> proved in principle.


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