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 00:37:42 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!logbridge.uoregon.edu!arclight.uoregon.edu!news.tufts.edu!uunet!dca.uu.net!ash.uu.net!lore.csc.com!baen1673807.greenlnk.net!baen1673807!not-for-mail From: "Phil Thornley" Newsgroups: comp.lang.ada Subject: Re: SPARK or RAVENSCAR (from "Re: www.ada-ru.org") Date: Wed, 5 Feb 2003 08:37:38 -0000 Organization: Computer Sciences Corporation Message-ID: <3e40cd05@baen1673807.greenlnk.net> References: <3e3ab8ff$1@epflnews.epfl.ch> NNTP-Posting-Host: 20.44.240.33 X-Trace: lore.csc.com 1044434261 13334 20.44.240.33 (5 Feb 2003 08:37:41 GMT) X-Complaints-To: abuse@news.csc.com NNTP-Posting-Date: Wed, 5 Feb 2003 08:37:41 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 5.00.2919.6600 X-MimeOLE: Produced By Microsoft MimeOLE V5.00.2919.6600 X-Original-NNTP-Posting-Host: waec857.wa.bae.co.uk X-Original-Trace: 5 Feb 2003 08:36:21 GMT, waec857.wa.bae.co.uk Xref: archiver1.google.com comp.lang.ada:33797 Date: 2003-02-05T08:37:38+00:00 List-Id: "Colin Paul Gloster" 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