Re: Array initialization in SPARK

[Alexander Senier <mail@senier.net>]

On Thu, 28 Oct 2010 08:23:19 -0700 (PDT)
"Peter C. Chapin" <pcc482719@gmail.com> wrote:

> My understanding is that SPARK assumes there are no flow errors when
> creating verification conditions. Thus, in general, if one accepts
> certain flow errors would there be a danger that one might
> subsequently prove a VC that is not really relevant to the program?

In Section 7.1 (and particularly in 7.1.1 "Array initialization in a
loop") of the SPARK Proof manual this issue is discussed. When
generating RTCs the Examiner *assumes* that all elements of an array are
defined and within their subtype ranges. The best way to ensure that
indeed is making the Examiner to show the absence of data flow errors.

If you must initialize arrays in a loop (as in your example), you have
to accept the flow errors and review the code to initialize all array
elements correctly. You definitely want to be very careful with those
accept statements and really simplify your other initialization
functions to make that as obvious as possible.

It may be benificial to restrict the initialization to simple patterns
that could be verified (semi-)automatically in the future. E.g. have a
for loop over the complete array index and only use its loop variable
to index into the array on the left-hand side of an assignment. If the
array is not referenced on the right-hand side (or only indices smaller
than the current value of the loop variable), all array elements should
be valid after execution of that loop. But your problem may not fit
into that pattern...

Regards,
Alex