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,30dadda29086c616,start X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-06-24 10:01:55 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: ANN: High-Integrity Ravenscar paper now available on-line Date: 24 Jun 2003 10:01:53 -0700 Organization: http://groups.google.com/ Message-ID: NNTP-Posting-Host: 62.173.119.178 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Trace: posting.google.com 1056474114 29486 127.0.0.1 (24 Jun 2003 17:01:54 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: 24 Jun 2003 17:01:54 GMT Xref: archiver1.google.com comp.lang.ada:39680 Date: 2003-06-24T17:01:54+00:00 List-Id: I'm pleaed to announce a new paper from SPARK Team - "High Integrity Ravenscar" by Peter Amey and Brian Dobbing. This paper was presented last week at the Ada Europe confernce in Toulouse. PDF is now available on the publications page of www.sparkada.com This paper provides the first public preview of what's coming in the next release of the SPARK language and toolset. Abstract: The Ravenscar Profile is an exciting development for the Ada community since it provides, for the first time in the history of our industry, support for deterministic, multi-tasking programming as an integral part of a standardized language. Despite its many advantages, the profile leaves several areas where behaviour is implementation defined and can result in run-time errors; this is unfortunate in a profile aimed clearly at the critical systems market. The SPARK language is a well-established sequential Ada subset that avoids ambiguity and allows all language rule violations to be detected prior to execution. The authors show how the principles of SPARK have been successfully extended to encompass the Ravencar Profile thereby statically eliminating the profile?s problematic areas. The result should allow concurrent Ada programs to be constructed with the same degree of rigour that is now possible using sequential SPARK. - Rod Chapman, SPARK Team, Praxis Critical Systems