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.99.54.3 with SMTP id d3mr30325212pga.116.1480975304381;
        Mon, 05 Dec 2016 14:01:44 -0800 (PST)
X-Received: by 10.157.37.125 with SMTP id j58mr3804891otd.18.1480975304316;
 Mon, 05 Dec 2016 14:01:44 -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!p16no3014779qta.1!news-out.google.com!m27ni1906qtf.1!nntp.google.com!n6no3015721qtd.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Mon, 5 Dec 2016 14:01:43 -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=156.57.114.26;
 posting-account=qa2LvwoAAADwbTxJVBI5rHWSlh3aClXp
NNTP-Posting-Host: 156.57.114.26
References: <c1a607a7-dce1-47a2-b4e5-7eba44ad4647@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <0bba1203-42cf-4689-afd1-c417c681f5f6@googlegroups.com>
Subject: Re: Ada features supported by SPARK 2014
From: Daniel King <daniel.dmk@googlemail.com>
Injection-Date: Mon, 05 Dec 2016 22:01:44 +0000
Content-Type: text/plain; charset=UTF-8
Xref: news.eternal-september.org comp.lang.ada:32622
Date: 2016-12-05T14:01:43-08:00
List-Id: <comp.lang.ada>

On Monday, 5 December 2016 16:36:20 UTC-4, paul...@googlemail.com  wrote:
> Hi,
> 
> I'm thinking about learning Ada or SPARK. It's only for hobby use, not for work.
> 
> I've been looking for an overview of SPARK, in relation to the features of Ada, but haven't found too much on the internet.
> 
> Wikipedia says SPARK2014 is a well defined subset of Ada. It would be nice 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 compared to Ada.
> 
> Any good links would be appreciated, before I go and buy a book on Ada and/or SPARK.
> 
> Thx.

The SPARK User's Guide has a list of excluded Ada features that you should find useful for comparing SPARK and Ada capabilities: http://docs.adacore.com/spark2014-docs/html/ug/source/language_restrictions.html#excluded-ada-features

In addition, for tasking features, SPARK is limited to the "Ravenscar profile", which is basically a set of restrictions on Ada's tasking features, to permit static analysis for formal verification.

A couple of links for SPARK that I find useful are the language reference manual (LRM) and user's guide:
  * LRM: http://docs.adacore.com/spark2014-docs/html/lrm/
  * User's guide: http://docs.adacore.com/spark2014-docs/html/ug/index.html