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

["Phil Thornley" <phil.thornley@baesystems.com>]

"Colin Paul Gloster" <Colin_Paul_Gloster@ACM.org> wrote in message
news:slrnb3vm4q.eb3.Colin_Paul_Gloster@camac.dcu.ie...
> In article news:3e3ab8ff$1@epflnews.epfl.ch , Rodrigo Garcia wrote
> in response to a post by Dmitriy Anisimkov:
>
> "    I have seen that, among the links you have added, you have
included the
> ORK page. As one of the project developers of ORK, I am very proud of
it.
> [..] you can read SPARK (the High-Integrity version of Ada) [..]"
>
> Hello Rodrigo.
>
> SPARK typically involves more dedication to proofs but Ravenscar is
not
> intended to be low integrity I would think. Do you think that SPARK is
> typically safer (for space work)?

SPARK and Ravenscar can't be compared because they address different
aspects of the language.

- The Ravenscar profile is explicitly silent on the sequential part of
the language.
- The SPARK language is (currently) limited to sequential programs.

So there is an excellent case for using them both - restrict the tasking
features used to conform to Ravenscar and analyse each task as a
separate SPARK program.

In fact this is such a good idea that the SPARK developers are planning
to add Ravenscar compliant features to the next version of SPARK. :-)


The guide to Ravenscar has recently been completed by the HRG. It is
published initially as a University of York report:

ftp://ftp.cs.york.ac.uk/reports and click on YCS-2003-348.pdf

and will be offered to WG9 as a potential ISO technical report.

Cheers,

Phil

--
Phil Thornley
BAE SYSTEMS