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,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: 103376,25e091afe1184988
X-Google-Attributes: gid103376,public
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!postnews.google.com!h48g2000cwc.googlegroups.com!not-for-mail
From: roderick.chapman@googlemail.com
Newsgroups: comp.lang.ada
Subject: Re: Reference-oriented language and high-integrity software
Date: 3 Nov 2006 01:43:18 -0800
Organization: http://groups.google.com
Message-ID: <1162546998.925808.52360@h48g2000cwc.googlegroups.com>
References: <eiet3r$2on$1@cernne03.cern.ch><87mz78zz1w.fsf@ludovic-brenta.org>
   <eif0qu$4k8$1@cernne03.cern.ch>
NNTP-Posting-Host: 217.205.167.137
Mime-Version: 1.0
Content-Type: text/plain; charset="iso-8859-1"
X-Trace: posting.google.com 1162547005 18766 127.0.0.1 (3 Nov 2006 09:43:25
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Fri, 3 Nov 2006 09:43:25 +0000 (UTC)
In-Reply-To: <eif0qu$4k8$1@cernne03.cern.ch>
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-GB;
 rv:1.8.1) Gecko/20061010 Firefox/2.0,gzip(gfe),gzip(gfe)
X-HTTP-Via: 1.1 bloxx:3128 (squid/2.5.STABLE11)
Complaints-To: groups-abuse@google.com
Injection-Info: h48g2000cwc.googlegroups.com; posting-host=217.205.167.137;
   posting-account=EhC47gwAAABJYiJ7JUJjwDyYMTWH1OKq
Xref: g2news2.google.com comp.lang.ada:7350
Date: 2006-11-03T01:43:18-08:00
List-Id: <comp.lang.ada>

The provision of _sound_ (i.e. no false negatives) and _fast_ aliasing
analysis
a key factor, even in the absence of dynamic memory and garbage
collection.

The soundness (and efficiency) of the information flow analyser
and the VC Generator (which is basically an implementation
of Hoare's assignment axiom) depend on this property.
 - Rod, SPARK Team