Prev: Two miscellaneous questions about GPS : Ada indentation andthen SPARK integration
Next: SPARK : surprising failure with implication
From: Yannick Duchêne (Hibou57) on 8 Jun 2010 12:40
Le Tue, 08 Jun 2010 09:23:53 +0200, Maciej Sobczak
<see.my.homepage(a)gmail.com> a écrit:
> This bug (and some others) is there for a long time already, but
> apparently nobody cares.
May be more people are using a news-reader instead of Google group so too
few body noticed ?

--
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.
First  |  Prev  | 
Pages: 1 2
Prev: Two miscellaneous questions about GPS : Ada indentation andthen SPARK integration
Next: SPARK : surprising failure with implication