Re: Question about SPARK flow error.

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

On 20 June, 01:37, "Peter C. Chapin" <pcc482...@gmail.com> wrote:
> Phil Thornley wrote:
> > The best way to deal with the error is an accept annotation.
> > Such an annotation is a potential risk as it may hide a genuine data
> > flow error (if not now then maybe when the code is changed at some
> > point in the future).
>
> Thanks for the suggestion. It sounds reasonable. What I did (at least for now)
> is more like a "junk initialization" although perhaps not complete junk. If
> the item is not found then Index gets Next_Index. So I started the procedure
> off with
>
>         Index := Next_Index;
>
> and removed that assignment from the condition when the item is not found. If
> the item is found inside the loop, Index gets overridden by a different
> value. Note that Next_Index is definitely initialized properly; my
> annotations declare it as a global in out variable and I have an
> initialization procedure (elsewhere) that sets it up.

That sounds like a reasonable solution in this case.

> I can see the danger to this... if I forgot to set Index inside the loop (or
> if that assignment gets removed later) the Examiner won't notice the problem.
> However, at least I can initialize Index to a semantically meaningful value.

I think that there is sometimes a tendency to expect more of the
Examiner than it can deliver - eliminating flow errors does not
guarantee correctness of the code, it just reduces the opportunities
for errors.

There may be some mileage in using check annotations to justify the
use of accept annotations for data flow errors - I'm going to think
about that one a little more.

Cheers,

Phil