Re: Local vs global variables in ADA

[rod@praxis-cs.co.uk (Rod Chapman)]

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