From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.31.114.14 with SMTP id n14mr7020831vkc.0.1480972240487;
        Mon, 05 Dec 2016 13:10:40 -0800 (PST)
X-Received: by 10.157.18.211 with SMTP id g77mr3796011otg.14.1480972240447;
 Mon, 05 Dec 2016 13:10:40 -0800 (PST)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.glorb.com!p16no2992538qta.1!news-out.google.com!j8ni5737qtc.0!nntp.google.com!p16no2992536qta.1!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Mon, 5 Dec 2016 13:10:39 -0800 (PST)
In-Reply-To: <c1a607a7-dce1-47a2-b4e5-7eba44ad4647@googlegroups.com>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=67.0.242.189;
 posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC
NNTP-Posting-Host: 67.0.242.189
References: <c1a607a7-dce1-47a2-b4e5-7eba44ad4647@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <dc507cef-4532-4a1d-a991-7061a360fb55@googlegroups.com>
Subject: Re: Ada features supported by SPARK 2014
From: Shark8 <onewingedshark@gmail.com>
Injection-Date: Mon, 05 Dec 2016 21:10:40 +0000
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
Xref: news.eternal-september.org comp.lang.ada:32620
Date: 2016-12-05T13:10:39-08:00
List-Id: <comp.lang.ada>

On Monday, December 5, 2016 at 1:36:20 PM UTC-7, paul...@googlemail.com wro=
te:
> Hi,
>=20
> I'm thinking about learning Ada or SPARK. It's only for hobby use, not fo=
r work.
>=20
> I've been looking for an overview of SPARK, in relation to the features o=
f Ada, but haven't found too much on the internet.
>=20
> Wikipedia says SPARK2014 is a well defined subset of Ada. It would be nic=
e to get a feel for how much of Ada is in SPARK, what are the main aspects =
of Ada not supported by SPARK, and what are SPARK's main limitations compar=
ed to Ada.
>=20
> Any good links would be appreciated, before I go and buy a book on Ada an=
d/or SPARK.
>=20
> Thx.

One of the nice things is that SPARK 2014 is a true subset of Ada 2012 (rat=
her than an annotated-comment system), meaning that ALL SPARK programs are =
valid Ada ones -- but probably the reason that you're having some difficult=
y is because SPARK is now fairly fine-grained so that you can easily use fu=
ll-Ada where you need to.

   Package Example with SPARK_Mode is
     Function SPARK_Function( X : Integer ) return Integer;
  =20
     Function NONSPARK_Function( X : Integer ) return Integer
       with SPARK_Mode =3D> Off;
   End Example;

I've been teaching myself SPARK recently, and I have found lists of feature=
s not in SPARK... but it was a while ago, and I didn't save a link.