Re: Array initialization in SPARK

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

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