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.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,2c0fbdd9804eddab
X-Google-Attributes: gid103376,public
From: Rod Chapman <rod@praxis-cs.co.uk>
Subject: Re: c/c++ now safer than Ada. a new tool.
Date: 1999/02/18
Message-ID: <36CBE623.9EDA4817@praxis-cs.co.uk>#1/1
X-Deja-AN: 445646403
Content-Transfer-Encoding: 7bit
References: <7af49j$hti@drn.newsguy.com> <7af7ri$fsj$1@cnn.Princeton.EDU>
 <36CB3D0C.F01D3CD@pwfl.com> <7afuj4$8ic$1@nnrp1.dejanews.com>
Content-Type: text/plain; charset=us-ascii
Organization: Praxis plc, U.K.
Mime-Version: 1.0
Newsgroups: comp.lang.ada
Date: 1999-02-18T00:00:00+00:00
List-Id: <comp.lang.ada>

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