Re: SPARK code samples

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

Le Thu, 12 Aug 2010 07:02:22 +0200, Jeffrey Carter  
<spam.jrcarter.not@spam.not.acm.org> a écrit:
> A .. B is the null range. I think you meant B .. A.
Yes. Erroneous copy/paste of a similar comment above or below.
This kind of error cannot be checked by SPARK :p
Apologize.


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