Re: SPARK code samples

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

Le Wed, 11 Aug 2010 18:45:33 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> 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)
You may also add some requirements not really expressable in term features  
exclusion, and rather in terms of constructions, like the requirement to  
have a single exit point (multiple return statements are not allowed).  
This kind-of is not a feature matter, this is an execution flow matter.  
This kind of requirements are enforced by the SPARK grammar.


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