Re: SPARK: What does it prove?

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

Le Mon, 31 May 2010 03:17:32 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> If is funny to note that these difficulty are a consequence of SPARK  
> tied to Ada. An example : Ada has modular type, but can't see modular  
> types has polynomials, and the relevant modal, which could help, would  
> be this one : polynomial. Has Ada don't has this, SPARK doesn't too.
Typo errors : replace Has by As every where it is relevant.
Sorry, it seems when I am writing, I mostly write words as a whole instead  
of writing letters one by one, so it happens I replace a word by another.

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