Re: Ada features supported by SPARK 2014

[Shark8 <onewingedshark@gmail.com>]

On Monday, December 5, 2016 at 1:36:20 PM UTC-7, 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.

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

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

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