Re: Ada features supported by SPARK 2014

["G.B." <bauhaus@futureapps.invalid>]

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