From: Vinzent Hoefler <ada.rocks@jlfencey.com>
Subject: Re: SPARK or RAVENSCAR (from "Re: www.ada-ru.org")
Date: Tue, 04 Feb 2003 10:57:38 -0500
Date: 2003-02-04T10:57:38-05:00 [thread overview]
Message-ID: <jtno1b.282.ln@jellix.jlfencey.com> (raw)
In-Reply-To: slrnb3vm4q.eb3.Colin_Paul_Gloster@camac.dcu.ie
Colin Paul Gloster wrote:
> 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)?
Well, probably you cannot really compare these two.
Ravenscar ist just a profile on what Ada features to use and what not to
use. In this sense the concept (subset of existing language) might be
seen similar to SPARK. But SPARK is a Ada-subset language with
additional annotations for automatic proof and in some terms it is far
more restricted than plain Ravenscar.
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.
So, in this view SPARK programs look safer, yes. ;)
Vinzent.
--
I think every good Christian ought to kick Falwell right in the ass.
-- Barry Goldwater
next prev parent reply other threads:[~2003-02-04 15:57 UTC|newest]
Thread overview: 8+ messages / expand[flat|nested] mbox.gz Atom feed top
2003-01-27 16:27 An: www.ada-ru.org Dmitriy Anisimkov
2003-01-27 20:00 ` Larry Kilgallen
2003-01-28 9:07 ` Dmitriy Anisimkov
2003-01-31 17:57 ` www.ada-ru.org Rodrigo Garcia
2003-02-04 15:13 ` SPARK or RAVENSCAR (from "Re: www.ada-ru.org") Colin Paul Gloster
2003-02-04 15:57 ` Vinzent Hoefler [this message]
2003-02-05 12:01 ` Rod Chapman
2003-02-05 8:37 ` Phil Thornley
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox