Re: Processing array subsections, a newbie question.

[Phil Thornley <phil.jpthornley@gmail.com>]

On 13 June, 15:01, "Peter C. Chapin" <pcc482...@gmail.com> wrote:
[...]
> Thanks for the suggestion (by you and others) for using a loop exit. SPARK has
> some restrictions on how 'exit' can be used; I'm not sure if they will apply
> to my case or not, but I can look into it. In my case there is also a state
> machine involved and the exiting would have to take place inside a case
> statement inside the loop. I seem to recall that SPARK has an issue with
> exiting from nested control structures but I can experiment.

I don't think the state machine will make any difference, but you
certainly can't exit an enclosing loop when in a case arm - you have
to move the exit(s) to after the 'end case'.

This is not usually too much of a problem, but in your code it forces
the exit to come after the increment (assuming that this has to stay
in the case arm).

As you suggest elsewhere in this thread, it is a good idea to have
subtype constraints as tight as possible.  In the situation you
describe I would define a type (to replace your use of Natural) that
has one extra value at the end (for the Index_Fst variable).  Then
define the array index as a subtype that excludes that extra value.
This should allow the increment to stay in the case arm, with the exit
following after the case.

(BTW, if you haven't tried it yet, you will find that using
unconstrained arrays creates additional work when doing run-time
checks as the VCs generated by any reference to an array element use
the limits for that array object, not just the array index subtype).

Cheers,

Phil