Re: Spark and the Ada numerics annex

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

Le Tue, 10 Aug 2010 10:48:30 +0200, Ada novice <ycalleecharan@gmx.com> a  
écrit:

> My interests are purely in Scientific numerical programming
SPARK will applies, it does not target a specific application area. While  
you may feel it is less handy in some than in some others. If you ever  
feel SPARK looks too much stupid for some package or method, then may just  
hide it from SPARK and try to comment the best way ever possible too give  
a proof that although not checked by SPARK, this "should be good".

> The good things about SPARK is that it helps to make checks and hence
> get the programming right. Is it recommended to use SPARK even for
> very simple programs?
Not only this is possible, this is also recommended in some way. The  
smaller an application is, the less pain you will have to prove its  
correctness. SPARK does not take part in a reification process (like  
things would go with the B-method), so there is a lot of things which will  
seems obvious to you; SPARK may not know right away about you application.  
For this reason, this may be better to keep it simple. Don't forget you  
can Hide if ever required.

procedure Your_Method
is
   --# hide Your_Method
   ... Your proses comes here ...
   ... Your informal comments proving you designed it right comes here ...
end Random;

Just don't abuse it.

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