Re: Array initialization in SPARK

[Phil Clayton <phil.clayton@lineone.net>]

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