Spark and the Ada numerics annex

Spark and the Ada numerics annex

[Ada novice]

Hi, I became interested in taking a look at SPARK. I've browsed
through the freely available first chapter of Barnes's SPARK book and
I saw that SPARK doesn't seem to cover the Ada specialized annexes
(see Figure 1.1. Relatonship between SPARK and Ada on pp. 11).

My interests are purely in Scientific numerical programming with Ada
and the Ada numerics annex is important to me. Is it true that SPARK.
If I understand correctly, then simple mathematical functions like
SQRT are elementary functions that are part of the language Ada itself
and SPARK will recognize these elementary functions. But the extensive
vector and matrix manipulations as added in Ada 05 won't be recognized
by SPARK. Am I right?

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?

Thanks
YC

Re: Spark and the Ada numerics annex

[Rod Chapman]

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

Re: Spark and the Ada numerics annex

[Ada novice]

On Aug 10, 12:18 pm, Rod Chapman <roderick.chap...@googlemail.com>
wrote:
> 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.

YC

Re: Spark and the Ada numerics annex

[Yannick Duchêne (Hibou57)]

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.

Re: Spark and the Ada numerics annex

[Yannick Duchêne (Hibou57)]

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.

Re: Spark and the Ada numerics annex

[Ada novice]

Thanks Hibou57 Yannick Duchêne for all this information.

Vous etes francophone si je ne me trompe pas et je vous remercie pour
toutes ces informations.

Cordialement
YC

Re: Spark and the Ada numerics annex

[Yannick Duchêne (Hibou57)]

Le Tue, 10 Aug 2010 14:28:58 +0200, Ada novice <ycalleecharan@gmx.com> a  
écrit:
> Vous etes francophone si je ne me trompe pas et je vous remercie pour
> toutes ces informations.
Yes I am (no body's perfect, and I would be the last). If you would like,  
do you know there exist a french version of this news-group ?

news:fr.comp.lang.ada if you use a news reader
or
http://groups.google.com/group/fr.comp.lang.ada/topics
if you use Google Groups


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

Re: Spark and the Ada numerics annex

[Ada novice]

On Aug 10, 3:04 pm, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> do you know there exist a french version of this news-group ?
>
> news:fr.comp.lang.ada if you use a news reader
> orhttp://groups.google.com/group/fr.comp.lang.ada/topics
> if you use Google Groups

Thanks. I've read about it somewhere but never visited it until now
that you have provided a link. I stick to the English site assuming
that most interesting discussions will be posted here but I can see
now that the French site indeed have very interesting discussions
also. If I understand correctly, the French site is not a translation
of the present English site but it does contain distinct posts in
French.

Cordialement
YC