Re: SPARK or RAVENSCAR (from "Re: www.ada-ru.org")

[rod.chapman@praxis-cs.co.uk (Rod Chapman)]

Vinzent Hoefler <ada.rocks@jlfencey.com> wrote in message news:
> So, from what I know, I'd say most if not all SPARK programs would 
> conform to Ravenscar, but a Ravenscar conforming program is not 
> necessarily written in SPARK.

I'm pleased to say that the next release of the SPARK language and
toolkit will incorporate the Ravenscar Profile as a core part of
the SPARK language.  Simply put, SPARK will be a strict subset of the
Ravenscar Profile incorporating library level tasks, protected objects,
suspension objects, Ada.Real_Time and so on.

The language will, of course, be amenable to all the existing forms
of static analysis implemented by the Examiner, but will add:

1) Analysis to show that programs are free from Ravenscar-defined
erroneous behaviour, exceptions, bounded errors and so on.  For example,
SPARK will be statically free from priority ceiling violations,
entry queue length violations, and so on.

2) Information flow analysis at the partition-level.

3) and much more...

We will be presenting a tutorial on the combined "RavenSPARK" language
and its analysis at Ada Europe in Toulouse in June.

 - Rod Chapman, SPARK Team, Praxis Critical Systems