From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,6182a664d144508e
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2003-02-05 04:01:49 PST
Path: archiver1.google.com!postnews1.google.com!not-for-mail
From: rod.chapman@praxis-cs.co.uk (Rod Chapman)
Newsgroups: comp.lang.ada
Subject: Re: SPARK or RAVENSCAR (from "Re: www.ada-ru.org")
Date: 5 Feb 2003 04:01:49 -0800
Organization: http://groups.google.com/
Message-ID: <cf2c6063.0302050401.1451da12@posting.google.com>
References: <b13mii$bmg$1@ns.omskelecom.ru> <3e3ab8ff$1@epflnews.epfl.ch>
 <slrnb3vm4q.eb3.Colin_Paul_Gloster@camac.dcu.ie>
 <jtno1b.282.ln@jellix.jlfencey.com>
NNTP-Posting-Host: 213.155.153.242
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
X-Trace: posting.google.com 1044446509 27917 127.0.0.1 (5 Feb 2003 12:01:49
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: 5 Feb 2003 12:01:49 GMT
Xref: archiver1.google.com comp.lang.ada:33805
Date: 2003-02-05T12:01:49+00:00
List-Id: <comp.lang.ada>

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