Ada features supported by SPARK 2014

Ada features supported by SPARK 2014

[pault.eg]

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.

 

Re: Ada features supported by SPARK 2014

[Shark8]

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.

Re: Ada features supported by SPARK 2014

[Jacob Sparre Andersen]

Shark8 <onewingedshark@gmail.com> writes:

> One of the nice things is that SPARK 2014 is a true subset of Ada 2012

This is unfortunately wrong.

An Ada 2012 compiler, which doesn't know SPARK 2014 has to reject
practically any SPARK 2014 program, as Ada 2012 compilers aren't allowed
to ignore unknown aspects.

Greetings,

Jacob
-- 
"Computer language design is just like a stroll in the park.
 Jurassic Park, that is."                             -- Larry Wall

Re: Ada features supported by SPARK 2014

[G.B.]

On 05.12.16 21:36, pault.eg@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.


http://www.adacore.com/sparkpro/tokeneer/discovery/

It might use the original SPARK syntax which had formalized
comments, but is otherwise compatible with the current
Ada syntax of contracts.

My impression (largely based on the original SPARK language)
was that it makes you say everything you know, in source text.
Nothing is implicit. Little can be deferred to run-time.

Every subtype and every object created must have bounds known
to the proof machinery.

No access types, or pointers.

Tasks, if any, must be declared at the library level,
i.e. not nested in subprograms or in other tasks;
Ada profile Ravenscar is in effect.

https://www.testandverification.com/files/Multicore_challenge_sept_2010/Rod_Chapman_Altran_Praxis.pdf

There was/is no/limited support for generic units.

...


-- 
"HOTDOGS ARE NOT BOOKMARKS"
Springfield Elementary teaching staff

Re: Ada features supported by SPARK 2014

[Daniel King]

On Monday, 5 December 2016 17:48:45 UTC-4, G.B.  wrote:
> 
> There was/is no/limited support for generic units.

To clarify, SPARK language versions 83, 95, and 2005 had no support for generic units at all (as far as I know), but the latest version of SPARK has full support for generic units (as long as they don't use any Ada language features that are not allowed in SPARK).

One consequence of this is that you can't actually run the proof tools on a generic unit directly, since it's not known if it's in SPARK or not until the unit is instantiated (for example, what if one of the generic parameters is an access type, which is not allowed in SPARK). So the proof tools are run on each *instantiation* of a generic unit.

I've used generics heavily in one of my SPARK projects - a SHA-3 hashing library: https://github.com/damaki/libkeccak

Re: Ada features supported by SPARK 2014

[Daniel King]

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

Re: Ada features supported by SPARK 2014

[Simon Wright]

Daniel King <daniel.dmk@googlemail.com> writes:

> 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.

I found that - as soon as there's anything involving time - I couldn't
work out how to specify flow (when I "fixed" one problem, another would
pop up somewhere else; if I "fixed" that, the first would pop up
again). So I left it up to the tool to infer flow for itself according
to whatever arcane rules it wanted to (not really a satisfactory state
of affairs for something that's supposed to increase my confidence in
the code).

Re: Ada features supported by SPARK 2014

[Daniel King]

On Tuesday, 6 December 2016 05:17:56 UTC-4, Simon Wright  wrote:
> Daniel King <danie...@googlemail.com> writes:
> 
> > 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.
> 
> I found that - as soon as there's anything involving time - I couldn't
> work out how to specify flow (when I "fixed" one problem, another would
> pop up somewhere else; if I "fixed" that, the first would pop up
> again). So I left it up to the tool to infer flow for itself according
> to whatever arcane rules it wanted to (not really a satisfactory state
> of affairs for something that's supposed to increase my confidence in
> the code).

Do you mean using "delay until"?

In such cases I've found that I've needed the following annotations:

   with Global => (Input => Ada.Real_Time.Clock_Time),
   Depends => (null => Ada.Real_Time.Clock_Time);

Re: Ada features supported by SPARK 2014

[Robert Eachus]

On Monday, December 5, 2016 at 3:36:20 PM UTC-5, paul...@googlemail.com wrote:
> 
> I'm thinking about learning Ada or SPARK. It's only for hobby use, not for work.

Lots of good answers, but they skip the high level to dive into details.

There are lots of uses for SPARK, such as safety critical systems or complex tasking systems where SPARK is required, or in some cases SPARK will make complex programming easier.

But in any case, learn Ada, then add SPARK. In fact you may have significant programs where 80% of the code is just Ada, then when the setup is finished, the safety-critical or time-critical part is all that is executing, and 100% SPARK.
 

Re: Ada features supported by SPARK 2014

[Adam Jensen]

On 12/09/2016 03:24 AM, Robert Eachus wrote:
> There are lots of uses for SPARK, such as safety critical systems or complex tasking systems where SPARK is required, or in some cases SPARK will make complex programming easier.

[That's quite a stutter you've got there, Bob]
(https://youtu.be/hrcDNKwWszA?t=19s). Are you innately inclined towards
fandom, fanaticism, and fetishism or do you believe exposure to computer
programming documentation might have induced some kind of semantic
obsessive-compulsive disorder in your thought and use of language? In
the case of the latter, I wonder if the publishers, editors, and/or
authors could be held liable? A lawsuit would be a hilarious way to
instigate change. (Something has to be done). The attention and
motivation manipulation methods of the finance capitalism money cults
<smirk> are no longer an occult technology. There are not sufficient
restrictions on petty, incompetent, and sociopathic applications of
those techniques <serious smirk>.

Joking aside, have any of you read from the electrical engineering or
chemistry corpus? In comparison, given the character of computer
programming documentation, how can anyone take it seriously?