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,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 2002:a24:6fd1:: with SMTP id x200mr4487355itb.26.1545187320078; Tue, 18 Dec 2018 18:42:00 -0800 (PST) X-Received: by 2002:a9d:2c22:: with SMTP id f31mr395670otb.4.1545187319932; Tue, 18 Dec 2018 18:41:59 -0800 (PST) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!feeder4.usenet.farm!feed.usenet.farm!weretis.net!feeder6.news.weretis.net!4.us.feeder.erje.net!feeder.erje.net!feeder.usenetexpress.com!feeder-in1.iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!q69no50235itb.0!news-out.google.com!v71ni17ita.0!nntp.google.com!k10no49775itk.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Tue, 18 Dec 2018 18:41:59 -0800 (PST) In-Reply-To: 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: <6f00bf64-d501-487c-b3cb-17e97346e801@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <8bd49bc7-ea3e-4e8c-9292-c37fd2e54e54@googlegroups.com> Subject: Re: New to Spark, working an example From: Brad Moore Injection-Date: Wed, 19 Dec 2018 02:42:00 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Xref: reader01.eternal-september.org comp.lang.ada:55076 Date: 2018-12-18T18:41:59-08:00 List-Id: On Sunday, December 16, 2018 at 2:48:19 AM UTC-7, Simon Wright wrote: > I don't think there's anything wrong with trying to attract attention > (what gets my goat a bit is people posting the same question in both > places at the same time). >=20 > I have to confess that I hadn't set up my SO account to watch the tags > [spark-2014] or [spark-ada] (why both?), or even [gnat] or [ada2012] - > rectified. You would have got more views if you'd included [ada] (but > not necessarily any (more) answers :) >=20 > Your problems are an indication of why I, as a person who has no access > to professional SPARK support, haven't invested any effort to speak of > in SPARK (my difficulties were with tasking/time rather than > mathematical loops, which tend to be rare in control systems). >=20 > That said, it looks to me as though the version of gnatprove in GNAT CE > 2018 may not fully understand exponentiation: >=20 > util.ads:3:14: medium: postcondition might fail, cannot prove 2 ** Floor_= Log2'Result <=3D X > util.ads:3:16: medium: overflow check might fail (e.g. when Floor_Log2'Re= sult =3D 0) I am by no means a SPARK expert, but I am also interested in exploring SPAR= K capabilities.=20 My approach led me to the following solution using just the SPARK 2018 GPL = download from Adacore.... (no extra provers were needed here, other than th= e ones that come with GNAT CE 2018) As an aside, it appears the version of gnatprove in GNAT CE 2018 does have = a pretty good understanding of exponentiation, given that I was able to get= the following proven. package Util with SPARK_Mode is =20 Max_Log2 : constant :=3D Positive'Size - 1; =20 subtype Log_Result is Natural range 0 .. Max_Log2; =20 function Floor_Log2 (X : Positive) return Log_Result with Global =3D> null, Depends =3D> (Floor_Log2'Result =3D> X), Post =3D> X >=3D 2**Floor_Log2'Result and then X / 2 < 2**Floor_Log2'Result; end Util; pragma Ada_2012; package body Util with SPARK_Mode is function Floor_Log2 (X : Positive) return Log_Result is begin -- Floor_Log2 =20 Log_Loop : for I in Log_Result loop pragma Loop_Invariant (for all J in 0 .. I =3D> X >=3D 2**J); pragma Assert(X / 2 < 2**Log_Result'Last); if X / 2 < 2**I then pragma Assert (X >=3D 2**I); pragma Assert (X / 2 < 2**I); return I; end if; =20 pragma Assume(I /=3D Log_Result'Last); =20 end loop Log_Loop; =20 return Log_Result'Last; =20 end Floor_Log2; =20 end Util; I technically didn't need to use the Global aspect or the Depends Aspect to= prove this function, but I think it is a good idea to provide a more detai= led contract using additional SPARK and Ada features, when possible.=20 The approach I took is to first of all make use of Ada 2012 contracts to co= nstrain the results to only allow valid values. The Log_Result subtype only= includes valid result values. I think this is an important goal in general to eliminate bugs, whether wri= ting code for regular Ada as well as SPARK.=20 My view is that in general, types such as Integer and Float should not be u= sed since they are types that describe memory storage, not types that descr= ibe values of interest in the application domain. By creating types that more accurately represent the application domain, I = believe it makes the job of writing proofs in SPARK much easier, since the = prover can reason that the values assigned to such values have specific val= ue ranges and properties. Another point, is to try to write an implementation that is easier to prove= . For that reason, I wrote this is a for loop rather than a while loop, bec= ause the compiler can reason statically about how many iterations are perfo= rmed, and what the values of the loop parameters can be. The prover was able to prove all the assertions in the implementation. I had to leave in one assumption, (the pragma assume),=20 pragma Assume(I /=3D Log_Result'Last); Without that, the prover complains that the post condition,=20 X / 2 < 2**Floor_Log2'Result cannot be proven. It appears that the prover is not able to prove that the = loop exited by the return statement, rather than iterating the full loop an= d exiting the loop without entering the if statement. However, I think this can be visually inspected and confirmed to be true, since the assert for the if statment, pragma Assert(X / 2 < 2**Log_Result'Last); just prior to the if statement was proven. It follows that if the assertion is true, then the if statement would have to be entered on the following line, and that the return would exit the loo= p. Thus, the reader should be able to visually tell that it is impossible to g= et by the if statement when I =3D Log_Result'Last, and thus the pragma Assu= me is true. The return at the end of the function should never get executed, as the onl= y way to exit the function is via the return inside the loop. I didn't need to have the return inside the loop for the purpose of proving= the function. I just did that to eliminate the need of extra variable decl= arations. Probably the prover could be improved so that such an assume could be elimi= nated while still proving the overall function. There may be a way to add additional asserts or pragmas to eliminate the ne= ed for the pragma Assume. So far I haven't found any, but perhaps someone e= lse might come up with a way. Otherwise, I'm pretty happy with the solution= I ended up with, given that the one assume in the code can be visually che= cked easily for correctness. I am sure that other SPARK solutions exist. I think when it comes to provin= g something, it is better to start with something simple, and to have in mi= nd choosing an implementation that is easier to prove. This should make it = easier to arrive at a proof. Brad