Re: Ada features supported by SPARK 2014

[Daniel King <daniel.dmk@googlemail.com>]

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