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,8002154d2966e1a1
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2002-11-06 07:40:55 PST
Path: archiver1.google.com!postnews1.google.com!not-for-mail
From: rod@praxis-cs.co.uk (Rod Chapman)
Newsgroups: comp.lang.ada
Subject: Re: Local vs global variables in ADA
Date: 6 Nov 2002 07:40:55 -0800
Organization: http://groups.google.com/
Message-ID: <ba18d5cb.0211060740.61af07eb@posting.google.com>
References: <5Ldx9.3695$151.38236@weber.videotron.net>
 <3DC5D1B7.1060707@acm.org>
 <PBux9.1632$Bd4.12716@dfw-service2.ext.raytheon.com> <3DC6DD54.10200@acm.org>
 <uadkov23t.fsf@FWILSON.i-did-not-set--mail-host-address--so-shoot-me>
 <u3cqg9b8l.fsf@gsfc.nasa.gov> <wcc4ravfxs0.fsf@shell01.TheWorld.com>
NNTP-Posting-Host: 213.155.153.242
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
X-Trace: posting.google.com 1036597255 7822 127.0.0.1 (6 Nov 2002 15:40:55
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: 6 Nov 2002 15:40:55 GMT
Xref: archiver1.google.com comp.lang.ada:30464
Date: 2002-11-06T15:40:55+00:00
List-Id: <comp.lang.ada>

Robert A Duff <bobduff@shell01.TheWorld.com> wrote in message news:
> I seem to recall some issue in SPARK, where they discouraged while
> loops.  Something about wanting to put a loop-invariant before the exit
> condition?  Maybe one of the SPARK folks can comment on that.

Not really - while loops are fine in SPARK.  You can place an assertion
either after the implicit loop exit, thus:

while A loop
   --# assert ... ;
   S;
end loop;

or before it:

while A
--# assert ... ;
loop
   S;
end loop;

or anywhere else in the loop body for that matter.  Note that the first form
does result in an additiona basic path (bypasses the assertion) for the
zero-iterations case.

The rules for placing exit statements in SPARK ensure that the resulting
flow graph is both reducible and can be generated from a semi-structured
graph grammar.  This property makes subsequent analyses (particularly
info flow analysis and verification condition generation) tractable.

 - Rod