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,5cb36983754f64da
X-Google-Attributes: gid103376,public
X-Google-Thread: 109fba,304c86061dc69dba
X-Google-Attributes: gid109fba,public
X-Google-ArrivalTime: 2004-02-17 00:25:23 PST
Path: 
 archiver1.google.com!news2.google.com!fu-berlin.de!uni-berlin.de!62.173.119.178!not-for-mail
From: Peter Amey <peter.amey@praxis-cs.co.uk>
Newsgroups: comp.lang.ada,comp.lang.c++
Subject: Re: No call for Ada (was Re: Announcing new scripting/prototyping
 language)
Date: Tue, 17 Feb 2004 08:26:19 +0000
Message-ID: <c0sj5h$1akqgu$1@ID-69815.news.uni-berlin.de>
References: <20040206174017.7E84F4C4114@lovelace.ada-france.org>
 <mailman.3.1076142690.295.comp.lang.ada@ada-france.org>
 <m3isij11u4.fsf_-_@insalien.org>
 <54759e7e.0402071124.322ea376@posting.google.com>
 <2460735.u7KiuvdgQP@linux1.krischik.com>
 <54759e7e.0402081525.50c7adae@posting.google.com>
 <m3fzdlyrh1.fsf@insalien.org>
 <MPG.1a93b9e1697e47b4989c8c@news.clspco.adelphia.net>
 <c0e5su$33j$1@titan.btinternet.com>
 <MPG.1a949d1f4c022540989c8f@news.clspco.adelphia.net>
 <c0esdi$63s$1@msunews.cl.msu.edu>
 <MPG.1a9555bd517ba66d989c91@news.clspco.adelphia.net>
 <x0eYb.6712$tL3.1375@newsread1.news.pas.earthlink.net>
NNTP-Posting-Host: 62.173.119.178
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii; format=flowed
Content-Transfer-Encoding: 7bit
X-Trace: news.uni-berlin.de 1077006322 44722718 I 62.173.119.178 ([69815])
User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US;
 rv:1.4) Gecko/20030624 Netscape/7.1 (ax)
X-Accept-Language: en-us, en
In-Reply-To: <x0eYb.6712$tL3.1375@newsread1.news.pas.earthlink.net>
Xref: archiver1.google.com comp.lang.ada:5625 comp.lang.c++:19346
Date: 2004-02-17T08:26:19+00:00
List-Id: <comp.lang.ada>



Richard Riehle wrote:

[snip]
> 
> C-Path compilers have their own problems.   The most well-known is the
> infamous "integer overflow" problem.   I recall that Tucker worked hard to
> eliminate this problem in his compiler (so it would pass validation).   I'm
> not
> sure what other compiler publishers are doing to avoid such problems, but
> as long as we require conformance testing (along with other kinds of
> testing)
> for Ada compilers chosen for weapons systems, we avoid some of those
> issues.

One of the nice properties of SPARK to C translation (to be described in 
our Ada Europe 2004 paper) is that we can constuct a proof at the SPARK 
level that all the numeric ranges will fit into the C types to which 
they will map and that overflows will therefore not occur.

Peter