Prev: Ada 2012: An Oops in the new Ada amendments ? (in 10.1.2 Context Clauses - With Clauses)
Next: Generic_Roots
From: Dmitry A. Kazakov on 11 Aug 2010 04:44
Since evidently growing interest in SPARK Ada and availability of public
SPARK compiler, I welcome those who are interested in learning and testing
SPARK to contribute their solutions to the Rosetta Code:

http://rosettacode.org/wiki/Main_Page

The Rosetta Code has a half of thousand programming tasks defined. The
tasks are solved almost any programming language ever existed. Ada is well
represented in Rosetta, but SPARK is not. (Clearly, not all tasks could be
implemented in SPARK)

Rosetta is pretty liberal, everyone can register and contribute. The
SPARK's page is:

http://rosettacode.org/wiki/SPARK

Thanks.

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
From: Ada novice on 11 Aug 2010 07:38
On Aug 11, 10:44 am, "Dmitry A. Kazakov" <mail...(a)dmitry-kazakov.de>
wrote:
>
> Rosetta is pretty liberal, everyone can register and contribute. The
> SPARK's page is:
>
>    http://rosettacode.org/wiki/SPARK

Thanks for this information. I'm interested to learn SPARK. If I
understand correctly, SPARK aligns itself well with Ada 95 and not yet
with Ada 05. Is this because of the strictness of SPARK to provide
highly reliable codes and hence it contains only well-tested features
(subset of Ada features)? It would be interesting to see some SPARK
codes on the wiki page building over time.

YC
From: Yannick Duchêne (Hibou57) on 11 Aug 2010 09:54
Le Wed, 11 Aug 2010 13:38:36 +0200, Ada novice <ycalleecharan(a)gmx.com> a
écrit:
> Is this because of the strictness of SPARK to provide
> highly reliable codes and hence it contains only well-tested features
> (subset of Ada features)?

Yes, this is the main reason, while this is not a barrier. It also have to
wait to be able to integrate Ada 2005, which cannot be done before the
required art and technique is there.

That said, SPARK slowly evolves toward the last Ada revision. Have a look
at this (just an example among others):
http://libre.adacore.com/libre/tools/spark-gpl-edition/

Which says
> A new SPARK 2005 language switch, enabling an initial set of
> new features for SPARK 2005. More features from Ada 2005 will
> be added to SPARK in future releases.

This cannot be done before proper formalization.... means this need time..

--
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 11 Aug 2010 11:26
Le Wed, 11 Aug 2010 10:44:58 +0200, Dmitry A. Kazakov
<mailbox(a)dmitry-kazakov.de> a écrit:
> http://rosettacode.org/wiki/Main_Page
I use to see reference to it from place to place. Just have a quick look a
few seconds ago. Is it on purpose if all examples seems to lack comments ?
I do not see any unsolved task for SPARK. Will have to first look at how
this site works prior anything.


--
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: Mark Lorenzen on 11 Aug 2010 12:07
On 11 Aug., 13:38, Ada novice <ycalleecha...(a)gmx.com> wrote:
>
> Thanks for this information. I'm interested to learn SPARK. If I
> understand correctly, SPARK aligns itself well with Ada 95 and not yet
> with Ada 05. Is this because of the strictness of SPARK to provide
> highly reliable codes and hence it contains only well-tested features
> (subset of Ada features)? It would be interesting to see some SPARK
> codes on the wiki page building over time.

Not quite. SPARK is a proper subset of Ada and is amenable to static
analysis. This has (in principle) nothing to do with if an Ada feature
is well-tested or not. You should think of SPARK as a language in its
own right and not as a subset of some other language. Although SPARK
constantly evolves it will never evolve into a language with the same
feature-set as Ada - no matter how well tested all Ada festures one
day will be.
 |  Next  |  Last
Pages: 1 2 3 4 5 6
Prev: Ada 2012: An Oops in the new Ada amendments ? (in 10.1.2 Context Clauses - With Clauses)
Next: Generic_Roots