Re: SPARK code samples

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

Le Wed, 11 Aug 2010 18:07:51 +0200, Mark Lorenzen  
<mark.lorenzen@gmail.com> a écrit:
> Not quite. SPARK is a proper subset of Ada and is amenable to static
> analysis.
Yes

> This has (in principle) nothing to do with if an Ada feature
> is well-tested or not.
SPARK is actually an Ada subset ;) And it elvoves toward more support of  
this or that Ada feature... while not all, and it will probably never  
support all, this one is true.

> You should think of SPARK as a language in its
> own right and not as a subset of some other language.
 From an abstract point of view, yes. There is SPARK and SPADE, and SPARK  
Examiner is based on SPADE Examiner (if I am not wrong... Rod will correct  
if needed). SPADE mainly came from Pascal, which was the first subsetted.  
But SPARK is still based on Ada. There is SPARK no SPARK Modula, no SPARK  
Oberon and so on.

> Although SPARK
> constantly evolves it will never evolve into a language with the same
> feature-set as Ada - no matter how well tested all Ada festures one
> day will be.
That precisely matter. If some feature are excluded, this is solely  
because they either does not enforce readability (overloading), are not  
predictable enough (while this depend on the state of the art) and could  
be in theory, but not practical or really workable way to do was found (if  
this end up into a SPARK which requires days to validate 10 lines, this is  
not good). Excluded features are excluded for some known reasons, most  
being documented in the SPARK Language Reference Manual.

By the way, the SPARK Language Reference Manual stick to the one Ada : it  
use the same section numbering, naming, and so on.

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