Re: Processing array subsections, a newbie question.

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Sun, 13 Jun 2010 16:01:20 +0200, Peter C. Chapin <pcc482719@gmail.com>  
a écrit:
> I seem to recall that SPARK has an issue with
> exiting from nested control structures but I can experiment.
>
> Peter
You have to exit from one to an outer one. Ex. if Loop1 includes Loop2  
which includes Loop3, you cannot “exit Loop1” from Loop3 (will look for  
the reference if needed).


-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.