Re: Spark and the Ada numerics annex

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

Le Tue, 10 Aug 2010 12:53:01 +0200, Ada novice <ycalleecharan@gmx.com> a  
écrit:
>> You can create a "shadow" specification of the various Numerics
>> packages to get at their facilities.  See section 13.1 of the book
>> on Shadows.
>>  - Rod, SPARK Team
>
> Thanks for this information. I don't have the book yet and I have been
> looking only at the first chapter which is freely available. I'll
> study this section when I get the book.
You can already get an idea right know (although the Barnes is still a  
must have recommended reading), if you have a look at this AdaGem :
http://www.adacore.com/2010/02/25/gem-80/

Basically, this is re-interfacing things so that SPARK does not get angry  
with what it sees.

By the way, this is a natural strategy, ... sure you would have though  
about it yourself. I've discovered this is named "shadow specification"  
just at the moment, reading Rod. I did not knew before this had this name.


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