Array initialization in SPARK

["Peter C. Chapin" <pcc482719@gmail.com>]

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