Re: Array initialization in SPARK

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

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