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=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,14da4c08f1736a33 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news2.google.com!postnews.google.com!u17g2000yqi.googlegroups.com!not-for-mail From: Phil Clayton Newsgroups: comp.lang.ada Subject: Re: Array initialization in SPARK Date: Fri, 29 Oct 2010 18:04:23 -0700 (PDT) Organization: http://groups.google.com Message-ID: References: <03b3b80e-9313-45b8-939a-7dde7780288c@y23g2000yqd.googlegroups.com> <3c36d3ba-6748-4aa9-9304-a219b11415bb@30g2000yql.googlegroups.com> <20101028182601.058336d9@senier-offen> NNTP-Posting-Host: 91.110.248.6 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1288400664 8350 127.0.0.1 (30 Oct 2010 01:04:24 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Sat, 30 Oct 2010 01:04:24 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: u17g2000yqi.googlegroups.com; posting-host=91.110.248.6; posting-account=v7gx3AoAAABfjb9m5b7l_Lt2KVEgQBIe User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (X11; U; Linux i686; en-GB; rv:1.9.0.15) Gecko/2009102704 Fedora/3.0.15-1.fc10 Firefox/3.0.15,gzip(gfe) Xref: g2news2.google.com comp.lang.ada:15921 Date: 2010-10-29T18:04:23-07:00 List-Id: On Oct 28, 5:38=A0pm, Phil Thornley wrote: > On 28 Oct, 17:26, Alexander Senier wrote: > [...]> It may be benificial to restrict the initialization to simple patt= erns > > 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) =3D> > --# =A0 =A0 =A0 =A0 (for J in Natural range Out_Matrix'Range(2) =3D> > --# =A0 =A0 =A0 =A0 =A0 =A0 (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 :=3D Matrix'(for I in Natural range Out_Matrix'Range(1) =3D> (for J in Natural range Out_Matrix'Range(2) =3D> 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