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-Received: by 2002:a0c:ea34:: with SMTP id t20mr67124666qvp.11.1564546850192; Tue, 30 Jul 2019 21:20:50 -0700 (PDT) X-Received: by 2002:aca:df08:: with SMTP id w8mr39772885oig.84.1564546849880; Tue, 30 Jul 2019 21:20:49 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!feeder.eternal-september.org!news.gegeweb.eu!gegeweb.org!usenet-fr.net!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!b26no8589084qtq.0!news-out.google.com!a5ni622qtd.0!nntp.google.com!b26no8589074qtq.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Tue, 30 Jul 2019 21:20:49 -0700 (PDT) In-Reply-To: <28e4ac2e-311b-40c4-ad81-42f55129ccd1@googlegroups.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=50.66.161.135; posting-account=lzqe5AoAAADHhp_gregSufVhvwu22fBS NNTP-Posting-Host: 50.66.161.135 References: <28e4ac2e-311b-40c4-ad81-42f55129ccd1@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Re: SPARK prooving an array of Positives. From: Brad Moore Injection-Date: Wed, 31 Jul 2019 04:20:50 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Xref: reader01.eternal-september.org comp.lang.ada:56985 Date: 2019-07-30T21:20:49-07:00 List-Id: I got this to prove in SPARK by making a couple of modifications. The first thing I noticed is that post conditions of First and Last are try= ing to show that the result is not larger than the Positive type maximum va= lue. I find it is a good idea to simplify the code, as it usually helps the proo= fing effort. If the result type of First and Last is of subtype Positive, t= hen there should be no need to prove anything, since Positive'Last =3D Max. So I changed the result type to Positive.=20 After doing that, the prover was happy about the First and Last functions, = but was complaining about the case statement when Item'Length is 2,=20 i.e. I had written,=20 when 2 =3D> return Unsigned_64(First * Last); SPARK wanted me to prove that this multiplication cannot cause a numeric ov= erflow. This is a problem now because First and Last are of type Positive, = and the result of multiplying the worst case positive values, Positive'Last= *Positive'Last would overflow, so I needed to convert the results of First = and Last to 64 bit unsigned values before doing the multiplication. The SPARK prover is now happy because it can tell that the multiplying the = two 31 bit values after converting to 64 bits will not overflow a 64 bit va= lue. I hope you don't mind, but I took the liberty of applying the GNAT style gu= idelines to the code, after turning on most style and warnings, and address= ing those. I also made a couple other changes that I thought might have hel= ped the prover, but I doubt was necessary, but something to keep in mind, a= nd seemed to be improvements, but I don't think any of these changes likely= helped the SPARK prover. For example, rather than use subtype Positive, and Interfaces.Unsigned_64, = I think it helped to define more specific types to fit the code problem. That is, instead of Positive, I defined type Axis_Value. This is a type def= inition, rather than a subtype definition. This might be helpful for SPARK = since the type definition is a compile-time definition, whereas subtypes ty= pically involve dynamic checking at run time to ensure that the range const= raints are being applied. I think generally SPARK would have an easier time= analyzing code if it can rely on compile time constraints.=20 I think also having the Axis_Value type declared makes it clearer in the co= de the number of bits associated with the type, rather than Positive, which= can be more target-dependent. Also, instead of using Interfaces.Unsigned_64, I defined the type Result_Va= lue, which seems to help clarify to the reader, and eliminate the need for = clients to with an extra package. package FITS with SPARK_Mode is type Result_Value is mod 2 ** 64; for Result_Value'Size use 64; type Axis_Value is range 1 .. +(2 **31 - 1); for Axis_Value'Size use 32; =20 type Axis_Count is range 0 .. 999 with Size =3D> 10; type Axis_Dimensions is array (Axis_Count range <>) of Axis_Value with Default_Component_Value =3D> 1; subtype Primary_Data_Array is Axis_Dimensions (1 .. 999); subtype Random_Groups_Data is Axis_Dimensions (1 .. 998); function EF (Item : FITS.Axis_Dimensions) return Result_Value; end FITS; package body FITS with SPARK_Mode is function EF (Item : FITS.Axis_Dimensions) return Result_Value is function First return Axis_Value is (Item (Item'First)) with Inline, Pre =3D> Item'Length > 0; function Last return Axis_Value is (Item (Item'Last)) with Inline, Pre =3D> Item'Length > 0; begin -- EF case Item'Length is when 0 =3D> return 1; when 1 =3D> return Result_Value (First); when 2 =3D> return Result_Value (First) * Result_Value (Last)= ; when others =3D> declare Middle : constant Axis_Count :=3D Item'Length / 2 + Item'Fir= st; subtype Head is Axis_Count range Item'First .. Middle; subtype Tail is Axis_Count range Axis_Count'Succ (Middle) .. Item'Last; begin return EF (Item (Head)) * EF (Item (Tail)); end; end case; end EF; end FITS; Brad