From: Rod Chapman <rod@praxis-cs.co.uk>
Subject: Re: c/c++ now safer than Ada. a new tool.
Date: 1999/02/18
Date: 1999-02-18T00:00:00+00:00 [thread overview]
Message-ID: <36CBE623.9EDA4817@praxis-cs.co.uk> (raw)
In-Reply-To: 7afuj4$8ic$1@nnrp1.dejanews.com
robert_dewar@my-dejanews.com wrote:
> Actually it seems to me that the extent to which it is
> possible to create such a tool is a direct indicator of
> the quality of the language design...
Absolutely - many of the more subtle and interesting semantic
analyses performed by the SPARK Examiner depend on the strength
of SPARK's language design. SPARK, for instance, eliminates
all semantic dependence on parameter passing mechanism,
alising and function side-effects. The Examiner also
manages these analyses in polynomial-time for realistic size
programs - which simply couldn't be done if it wasn't for the
simplicity and formality of the language in the first place!
(If you're interested in language design and are now thinking
"What's SPARK?", then I suggest you have a look - John Barnes'
most recent book is a good place to start.)
- Rod Chapman
Praxis Critical Systems
next prev parent reply other threads:[~1999-02-18 0:00 UTC|newest]
Thread overview: 6+ messages / expand[flat|nested] mbox.gz Atom feed top
1999-02-17 0:00 c/c++ now safer than Ada. a new tool mike
1999-02-17 0:00 ` Martin C. Carlisle
1999-02-17 0:00 ` Marin David Condic
1999-02-18 0:00 ` robert_dewar
1999-02-18 0:00 ` Rod Chapman [this message]
1999-02-17 0:00 ` Gautier
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox