Prev: installing SPARK GPL on Windows
Next: Bug rate and choice of programming language
From: Ada novice on 10 Aug 2010 04:48
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
From: Rod Chapman on 10 Aug 2010 06:18
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
From: Ada novice on 10 Aug 2010 06:53
On Aug 10, 12:18 pm, Rod Chapman <roderick.chap...(a)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
From: Yannick Duchêne (Hibou57) on 10 Aug 2010 07:40
Le Tue, 10 Aug 2010 12:53:01 +0200, Ada novice <ycalleecharan(a)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.
From: Yannick Duchêne (Hibou57) on 10 Aug 2010 08:09
Le Tue, 10 Aug 2010 10:48:30 +0200, Ada novice <ycalleecharan(a)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.
 |  Next  |  Last
Pages: 1 2
Prev: installing SPARK GPL on Windows
Next: Bug rate and choice of programming language