From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,14da4c08f1736a33
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news1.google.com!postnews.google.com!y23g2000yqd.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: Array initialization in SPARK
Date: Thu, 28 Oct 2010 05:47:53 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <03b3b80e-9313-45b8-939a-7dde7780288c@y23g2000yqd.googlegroups.com>
References: 
 <fc36c1af-120b-46d9-8c4c-5e5c990a2463@v20g2000yqb.googlegroups.com>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1288270073 6332 127.0.0.1 (28 Oct 2010 12:47:53
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Thu, 28 Oct 2010 12:47:53 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: y23g2000yqd.googlegroups.com; posting-host=80.177.171.182;
 posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64;
 Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR
 3.0.30729; Media Center PC 6.0; .NET4.0C),gzip(gfe)
Xref: g2news1.google.com comp.lang.ada:14894
Date: 2010-10-28T05:47:53-07:00
List-Id: <comp.lang.ada>

On 28 Oct, 11:13, "Peter C. Chapin" <pcc482...@gmail.com> wrote:
[...]
> =A0 =A0procedure Matrix_Transpose(In_Matrix : in Matrix; Out_Matrix : out
> Matrix) is
> =A0 =A0begin
> =A0 =A0 =A0 for I in Natural range Out_Matrix'Range(1) loop
> =A0 =A0 =A0 =A0 =A0for J in Natural range Out_Matrix'Range(2) loop
> =A0 =A0 =A0 =A0 =A0 =A0 Out_Matrix(I, J) :=3D In_Matrix(J, I);
> =A0 =A0 =A0 =A0 =A0end loop;
> =A0 =A0 =A0 end loop;
> =A0 =A0end 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
>
> =A0 =A0Out_Matrix :=3D (others =3D> (others =3D> 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) :=3D 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