Array initialization in SPARK

Array initialization in SPARK

[xorque]

Hello.

What's the correct way to initialize an array in SPARK?

Every method I've tried results in semantic or flow errors:

   9        Status (Index) := 0;
            ^
!!!        Flow Error        : 23: Statement contains reference(s) to
variable
           Status which has an undefined value.

   6      Status : Status_t := (others => 0);
                                ^
***        Syntax Error      : No EXPRESSION can start with reserved
word
           "OTHERS".

   7        (Status_Element_Index_t'First => 0,
                                          ^
***        Syntax Error      : No complete SIMPLE_EXPRESSION can be
followed by
           "=>" here.

And so on...

Re: Array initialization in SPARK

[xorque]

xorque wrote:
> Hello.
>
> What's the correct way to initialize an array in SPARK?

Status := Status_t'(Status_Element_Index_t => 0);

Array initialization in SPARK

[Peter C. Chapin]

Hello!

Consider the following type definition:

type Matrix is array(Natural range <>, Natural range <>) of
Types.Float8;

Now consider the following "obvious" implementation of a matrix
transpose procedure:

   procedure Matrix_Transpose(In_Matrix : in Matrix; Out_Matrix : out
Matrix) is
   begin
      for I in Natural range Out_Matrix'Range(1) loop
         for J in Natural range Out_Matrix'Range(2) loop
            Out_Matrix(I, J) := In_Matrix(J, I);
         end loop;
      end loop;
   end Matrix_Transpose;

This procedure makes assumptions about the relative sizes of the two
matrix objects. I intend to assert those assumptions using
preconditions. However, my question right now is about the
initialization of Out_Matrix. As written the Examiner complains that
the "initial undefined value of Out_Matrix is used in the definition
of Out_Matrix" (or words to that effect). I understand the issue. The
assignment inside the loop only assigns to a single matrix element at
a time. Thus, for example, the first time it executes the resulting
value of Out_Matrix has only one defined element; the rest of the
matrix has its "initial undefined value." I understand that SPARK
works this way because it can't be expected to track individual array
elements because array indexes are dynamic constructs.

In the past when I've had this problem I've just used an aggregate to
initialize the array. In full Ada I can do

   Out_Matrix := (others => (others => 0.0));

However, SPARK isn't happy with this. I'm having trouble figuring out
what would make SPARK happy here. Actually it would be even better if
I could convince the Examiner that the overall effect of the two loops
is to initialize the entire Out_Matrix. I'm not keen about spending
execution time with an aggregate initialization only to overwrite the
initial values anyway. In fact, SPARK complains about doing that sort
of thing with scalar values so it certainly doesn't seem like the
"SPARK way."

Peter

Re: Array initialization in SPARK

[Phil Thornley]

On 28 Oct, 11:13, "Peter C. Chapin" <pcc482...@gmail.com> wrote:
[...]
>    procedure Matrix_Transpose(In_Matrix : in Matrix; Out_Matrix : out
> Matrix) is
>    begin
>       for I in Natural range Out_Matrix'Range(1) loop
>          for J in Natural range Out_Matrix'Range(2) loop
>             Out_Matrix(I, J) := In_Matrix(J, I);
>          end loop;
>       end loop;
>    end Matrix_Transpose;
>
> This procedure makes assumptions about the relative sizes of the two
> matrix objects. I intend to assert those assumptions using
> preconditions. However, my question right now is about the
> initialization of Out_Matrix. As written the Examiner complains that
> the "initial undefined value of Out_Matrix is used in the definition
> of Out_Matrix" (or words to that effect). I understand the issue. The
> assignment inside the loop only assigns to a single matrix element at
> a time. Thus, for example, the first time it executes the resulting
> value of Out_Matrix has only one defined element; the rest of the
> matrix has its "initial undefined value." I understand that SPARK
> works this way because it can't be expected to track individual array
> elements because array indexes are dynamic constructs.
>
> In the past when I've had this problem I've just used an aggregate to
> initialize the array. In full Ada I can do
>
>    Out_Matrix := (others => (others => 0.0));
>
> However, SPARK isn't happy with this. I'm having trouble figuring out
> what would make SPARK happy here.

I don't think that you can get SPARK to accept an aggregate assignment
for an unconstrained array.  Section 4.1 of the LRM says:
"SPARK excludes most whole-array operations on unconstrained array
objects, in order that rules relating to index bounds may be
statically checked."

>                                    Actually it would be even better if
> I could convince the Examiner that the overall effect of the two loops
> is to initialize the entire Out_Matrix. I'm not keen about spending
> execution time with an aggregate initialization only to overwrite the
> initial values anyway. In fact, SPARK complains about doing that sort
> of thing with scalar values so it certainly doesn't seem like the
> "SPARK way."

It's far better to use the accept annotation (which is there for this
sort of situation):

   begin
      for I in Natural range Out_Matrix'Range(1) loop
         for J in Natural range Out_Matrix'Range(2) loop
            --# accept F, 23, Out_Matrix, "All of array is assigned in
the loop.";
            Out_Matrix(I, J) := In_Matrix(J, I);
            --# end accept;
         end loop;
      end loop;
   --# accept F, 602, Out_Matrix, Out_Matrix, "All of array is
assigned in the loop.";
   end Matrix_Transpose;


Cheers,

Phil

Re: Array initialization in SPARK

[Peter C. Chapin]

On Oct 28, 8:47 am, Phil Thornley <phil.jpthorn...@gmail.com> wrote:

> It's far better to use the accept annotation (which is there for this
> sort of situation):

Thanks for the suggestion. I can see the value of accept here.

In this case its pretty obvious that the entire output matrix is being
assigned. I have a couple of other procedures with a similar issue but
where it is much less obvious that they are setting values for all
matrix elements (they are supposed to be doing so). I can see that
while accept is a useful tool one would have to be careful about
sprinkling them around too liberally. I'll take a closer look at those
other procedures and see if a little code reorganization might be
desirable.

Thanks again!

Peter

Re: Array initialization in SPARK

[Peter C. Chapin]

On Oct 28, 10:51 am, "Peter C. Chapin" <pcc482...@gmail.com> wrote:

> Thanks for the suggestion. I can see the value of accept here.

I thought of a follow up question...

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?

Peter

Re: Array initialization in SPARK

[Alexander Senier]

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

Re: Array initialization in SPARK

[Phil Thornley]

On 28 Oct, 17:26, Alexander Senier <m...@senier.net> wrote:
[...]
> It may be benificial to restrict the initialization to simple patterns
> that could be verified (semi-)automatically in the future.
[...]

That's excellent advice.

But if you can't do that, and it really is important to ensure
complete initialization, and you are completing run-time check proofs,
then you could force a check on the array:

--# check for all I in Natural range Out_Matrix'Range(1) =>
--#         (for J in Natural range Out_Matrix'Range(2) =>
--#             (Out_Matrix(I, J) in Types.Float8));

but, for a complex initialization, completing the proof of this check
will be correspondingly complex :-(

Cheers,

Phil

Re: Array initialization in SPARK

[Phil Clayton]

On Oct 28, 5:38 pm, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
> On 28 Oct, 17:26, Alexander Senier <m...@senier.net> wrote:
> [...]> It may be benificial to restrict the initialization to simple patterns
> > that could be verified (semi-)automatically in the future.
>
> [...]
>
> That's excellent advice.
>
> But if you can't do that, and it really is important to ensure
> complete initialization, and you are completing run-time check proofs,
> then you could force a check on the array:
>
> --# check for all I in Natural range Out_Matrix'Range(1) =>
> --#         (for J in Natural range Out_Matrix'Range(2) =>
> --#             (Out_Matrix(I, J) in Types.Float8));
>
> but, for a complex initialization, completing the proof of this check
> will be correspondingly complex :-(

Whilst concious of sounding like a broken record, I feel compelled to
mention that this is exactly one of the reasons "for aggregates" (as
discussed recently on c.l.a.) would be a useful new Ada feature.  We
could then write something like:

  Out_Matrix :=
     Matrix'(for I in Natural range Out_Matrix'Range(1) =>
               (for J in Natural range Out_Matrix'Range(2) =>
                  In_Matrix(J, I)));

Any tool doing static analysis (compilers included) would know from
the syntax that the whole of the l.h.s. is written to.  Also, for a
side-effect free r.h.s, it can be seen that the order of iteration
does not affect its value.

Phil Clayton

Re: Array initialization in SPARK

[AdaMagica]

On 30 Okt., 03:04, Phil Clayton <phil.clay...@lineone.net> wrote:
> ...  We
> could then write something like:
>
>   Out_Matrix :=
>      Matrix'(for I in Natural range Out_Matrix'Range(1) =>
>                (for J in Natural range Out_Matrix'Range(2) =>
>                   In_Matrix(J, I)));

But we would need an assertion that 'Range(1) equals 'Range(2), else
we would get Constraint_Error. (Equal lengths would not suffice - no
sliding there.)

Re: Array initialization in SPARK

[Phil Clayton]

On Oct 30, 9:10 am, AdaMagica <christoph.gr...@eurocopter.com> wrote:
> On 30 Okt., 03:04, Phil Clayton <phil.clay...@lineone.net> wrote:
>
> > ...  We
> > could then write something like:
>
> >   Out_Matrix :=
> >      Matrix'(for I in Natural range Out_Matrix'Range(1) =>
> >                (for J in Natural range Out_Matrix'Range(2) =>
> >                   In_Matrix(J, I)));
>
> But we would need an assertion that 'Range(1) equals 'Range(2), else
> we would get Constraint_Error. (Equal lengths would not suffice - no
> sliding there.)

Yes, you would need Out_Matrix'Range(1) = In_Matrix'Range(2) and vice-
versa.
I actually meant to write:

  Out_Matrix :=
     Matrix'(for I in Natural range In_Matrix'Range(2) =>
               (for J in Natural range In_Matrix'Range(1) =>
                  In_Matrix(J, I)));

which still requires the same assertions.  However, this r.h.s. could
be used as the return value of a Matrix_Transpose function which would
enable us to avoid such assertions because we don't have to specify
the unconstrained array size independently, e.g.

  Out_Matrix : Matrix := Matrix_Transpose(In_Matrix);

I suppose this is a more 'functional' style of Ada...

Phil