Re: SPARK code samples

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

Le Wed, 11 Aug 2010 13:38:36 +0200, Ada novice <ycalleecharan@gmx.com> a  
écrit:
> Is this because of the strictness of SPARK to provide
> highly reliable codes and hence it contains only well-tested features
> (subset of Ada features)?

Yes, this is the main reason, while this is not a barrier. It also have to  
wait to be able to integrate Ada 2005, which cannot be done before the  
required art and technique is there.

That said, SPARK slowly evolves toward the last Ada revision. Have a look  
at this (just an example among others):
http://libre.adacore.com/libre/tools/spark-gpl-edition/

Which says
> A new SPARK 2005 language switch, enabling an initial set of
> new features for SPARK 2005. More features from Ada 2005 will
> be added to SPARK in future releases.

This cannot be done before proper formalization.... means this need time.

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