From: Peter Amey <pna@praxis-cs.co.uk>
Subject: Re: an you get this for me?
Date: 1998/06/11
Date: 1998-06-11T00:00:00+00:00 [thread overview]
Message-ID: <358057FA.1033@praxis-cs.co.uk> (raw)
In-Reply-To: 357FE61F.B8F81BFC@boeing.com
>
> 4. Safer C by Les Hatton discusses use of C in safety critical systems
> and contains a comparision with Ada.
>
I recommend treating this book with a certain amount of caution; it manages
to draw some rather bizarre conclusions.
For example, Les Hatton points to the existence of SPARK as some sort of
proof that Ada must be "dangerous" - why invent a secure subset if the
language is already "safe"? The reality, of course, is that it is only
_because_ the basic foundations of Ada are so good that is was possible to
define SPARK. A useable subset of C with SPARK's properties would be very
difficult to produce (and it certainly wouldn't be a high-level language
with support for abstraction etc.). A SPARK-like subset of C++ is probably
impossible.
Having dismissed Ada he then goes on to show that C is ok (providing you
don't make any mistakes) and you use rafts of (his) tools to bring checking
up to about the level of that performed by an Ada compiler.
George Romanski of Aonix has quite a good review of the book which I think
is available from their web site.
Safety-critical systems involve unique problems including the need to be
able to demonstrate, prior to any in-service experience, that the system
_will_ be safe when deployed. An essential basis for such a demonstration
is a programming language with clear semantics that can be reasoned about.
Ada is probably the only commercially-supported foundation on which such a
language can built.
--
---------------------------------------------------------------------------
__ Peter Amey, Product Manager
) Praxis Critical Systems Ltd
/ 20, Manvers Street, Bath, BA1 1PX
/ 0 Tel: +44 (0)1225 466991
(_/ Fax: +44 (0)1225 469006
http://www.praxis-cs.co.uk/
--------------------------------------------------------------------------
parent reply other threads:[~1998-06-11 0:00 UTC|newest]
Thread overview: expand[flat|nested] mbox.gz Atom feed
[parent not found: <357FE61F.B8F81BFC@boeing.com>]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox