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-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,a00006d3c4735d70
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2004-01-30 11:20:51 PST
Path: 
 archiver1.google.com!news2.google.com!news.maxwell.syr.edu!newshosting.com!nx02.iad01.newshosting.com!news-feed01.roc.ny.frontiernet.net!nntp.frontiernet.net!uunet.MISMATCH!ash.uu.net!spool.news.uu.net!not-for-mail
Date: Fri, 30 Jan 2004 14:20:19 -0500
From: Hyman Rosen <hyrosen@mail.com>
User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US;
 rv:1.5) Gecko/20031013 Thunderbird/0.3
X-Accept-Language: en-us, en
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: In-Out Parameters for functions
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>
 <bve0t4$r1pa9$1@ID-69815.news.uni-berlin.de>
In-Reply-To: <bve0t4$r1pa9$1@ID-69815.news.uni-berlin.de>
Content-Type: text/plain; charset=us-ascii; format=flowed
Content-Transfer-Encoding: 7bit
Organization: KBC Financial Products
Message-ID: <1075490424.476589@master.nyc.kbcfp.com>
Cache-Post-Path: master.nyc.kbcfp.com!unknown@nightcrawler.nyc.kbcfp.com
X-Cache: nntpcache 3.0.1 (see http://www.nntpcache.org/)
NNTP-Posting-Host: 204.253.250.10
X-Trace: 1075490424  10652 204.253.250.10
Xref: archiver1.google.com comp.lang.ada:5119
Date: 2004-01-30T14:20:19-05:00
List-Id: <comp.lang.ada>

Peter Amey wrote:
>> To be caught by a toolset requires whole-program analysis.
> 
> Not so in the case of SPARK.

As far as I know, SPARK has no way of calling procedures
except by explicitly mentioning their names. That is, there
are no procedure access variables, no generics, and no
dispatching. So it's no surprise that when you annotate a
declaration in enough detail to tell you what the body will
be doing, you can perform the analysis without seeing the
body. That's close to whole-program analysis in my book.

Also, SPARK doesn't allow side-effects in functions, so this
discussion is pretty moot from SPARK's point of view.

But Ada is not SPARK. Ada does have procedure access variables,
generics, dispatching, and side-effects, and the issues of
evaluation order are germane.

By the way, I read the paper to which you referred. What happens
in SPARK if I have
     package Sensor
     --# own in State;
     is
         function Value return Integer;
         --# global State;
     end Sensor;
and I try to write
     delta : Integer := Sensor.Value - Sensor.Value;

Can I write a function, not a procedure, which will return
different sensor values each time? Can I use them multiple
times in an expression?