ANN: High-Integrity Ravenscar paper now available on-line

[rod.chapman@praxis-cs.co.uk (Rod Chapman)]

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