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,a00006d3c4735d70
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2004-01-30 08:31:34 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
Subject: Re: In-Out Parameters for functions
Date: Fri, 30 Jan 2004 16:31:26 +0000
Message-ID: <bve0t4$r1pa9$1@ID-69815.news.uni-berlin.de>
References: <wcczncdrowb.fsf@shell01.TheWorld.com>
 <mailman.15.1075065014.2270.comp.lang.ada@ada-france.org>
 <wcc8yju2tjk.fsf@shell01.TheWorld.com>
 <1075159458.149886@master.nyc.kbcfp.com>
 <wcc4qui2sec.fsf@shell01.TheWorld.com>
 <d%jRb.1212$nR.528@nwrdny01.gnilink.net>
 <mailman.35.1075191506.2270.comp.lang.ada@ada-france.org>
 <1075225041.167448@master.nyc.kbcfp.com>
 <wccvfmxrw9q.fsf@shell01.TheWorld.com>
 <vcve10h7hhlc8pea4vu5pvr5035917i60r@4ax.com>
 <1075303237.975898@master.nyc.kbcfp.com>
 <9khh10pti0dn8gcp7f18ghptaifluj0fud@4ax.com>
 <1075390647.405841@master.nyc.kbcfp.com>
 <pan.2004.01.29.18.20.03.61778@email.ro>
 <1075405582.982776@master.nyc.kbcfp.com> <U5OdnRDGhvvVVITdRVn-sw@comcast.com>
 <1075478950.231615@master.nyc.kbcfp.com>
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 1075480292 28370249 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: <1075478950.231615@master.nyc.kbcfp.com>
Xref: archiver1.google.com comp.lang.ada:5100
Date: 2004-01-30T16:31:26+00:00
List-Id: <comp.lang.ada>



Hyman Rosen wrote:
> Robert I. Eachus wrote:
> 
>> will be caught by the SPARK toolset...
> 
>  > establish guidelines...
> 
> To be caught by a toolset requires whole-program analysis.
> [snip]

Not so in the case of SPARK.  The language design and the use of 
annotations means we can find things like function side effects and 
aliasing at the program unit level using computationally efficient 
techniques.  We can frequently find errors in programs that are not yet 
complete enough to compile.  That is why SPARK users typically run the 
Examiner about 10 times as often as they run the compiler (and about a 
million times as often as they run the debugger!).

See http://www.sparkada.com/downloads/sigada2001.pdf for an overview of 
how this all works.

Peter