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: 103376,6d79efdb8dde2c5a X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,CP1252 Path: g2news1.google.com!postnews.google.com!i31g2000yqm.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: SPARK : third example for Roesetta - reviewers welcome Date: Sun, 15 Aug 2010 11:42:27 -0700 (PDT) Organization: http://groups.google.com Message-ID: <589eea9a-0b14-4ae5-bf62-9abf4b33e7fb@i31g2000yqm.googlegroups.com> References: NNTP-Posting-Host: 80.177.171.182 Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1281897747 765 127.0.0.1 (15 Aug 2010 18:42:27 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Sun, 15 Aug 2010 18:42:27 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: i31g2000yqm.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:13354 Date: 2010-08-15T11:42:27-07:00 List-Id: On 15 Aug, 07:17, Yannick Duch=EAne (Hibou57) wrote: > Here is about the third example for Rosetta Code () Some comments first: > Position :=3D Index_Type'First; > -- Default value (required to not a have a data flow error). It's bad practice to put in an unnecessary assignment to get rid of a flow error. It is much better to structure the code to avoid the flow error. (They can hide genuine flow errors.) In this case you can get rid of this one by not defining the variable Middle and using Position instead - since Position is simply assigned to Middle once a value is found. > for Source_Index in > Binary_Searchs.Index_Type range Source'Range > loop > --# assert True; > -- No need for an assertion on anything. If you don't need an assertion then don't put one in. If you want to get rid of the warning about the default assertion then just put 'default_loop_assertions' into your warning file. > =A0 =A0 =A0 =A0 =A0 SPARK_IO.Put_Integer > =A0 =A0 =A0 =A0 =A0 =A0 (File =A0=3D> SPARK_IO.Standard_Output, > =A0 =A0 =A0 =A0 =A0 =A0 =A0Item =A0=3D> Source_Index, This line just prints the index - should be Item =3D> Source(Source_Index), > case Success is > when True =3D> A case statement for a Boolean is just a waste of typing. Also I don't think 'Success' is a good name for this variable as the program always 'succeeds'. 'Found' would be a more descriptive name and is more clearly a Boolean term. > begin > =A0 =A0 SPARK_IO.New_Line (File =3D> SPARK_IO.Standard_Output, Spacing = =3D> 1); > =A0 =A0 Run_Search (Source =3D> Array_Type'(0, 1, 2, 3, 4), Item =3D> 3); > =A0 =A0 Run_Search (Source =3D> Array_Type'(1, 2, 3, 4, 5), Item =3D> 3); > =A0 =A0 Run_Search (Source =3D> Array_Type'(1, 2, 3, 4, 5), Item =3D> 0); > =A0 =A0 Run_Search (Source =3D> Array_Type'(1, 2, 3, 4, 5), Item =3D> 6); > =A0 =A0 Run_Search (Source =3D> Array_Type'(1, 2, 3, 4, 5), Item =3D> 1); > =A0 =A0 Run_Search (Source =3D> Array_Type'(1, 2, 3, 4, 5), Item =3D> 5); > =A0 =A0 Run_Search (Source =3D> Array_Type'(1, 2, 3, 4, 5), Item =3D> 2); You might have noticed that error if these tests had been a bit more diverse! > * The test part, that is Run_Search and body of Program takes up to half = =A0 > of all of the source. Should I remove it or not ? I don't think so - it seems to be a good idea to provide runable programs where appropriate. > * In the loop inside of Search there are Check annotations which was not = =A0 > strictly needed but which I still left for more expressiveness. Is that O= K =A0 > ? Not too much ? I prefer user rules to large numbers of check annotations, but YMMV. > * To keep it simple so far, I have dropped a precondition which I =A0 > initially started with and which was requiring the array to be sorted. = =A0 > This only impact semantic, not runtime check, as any way, the subrange = =A0 > width always decrease, so that the loop always terminates. Should I or = =A0 > should I not get it back ? See my version below (which requires this precondition). > * I also though about an indirect way to prove the loop always terminates > (although this is not a feature supported by SPARK, there are indirect > ways to achieve this). I though this would look like too much obfuscated > if I add it. Do you agree this would be a bad idea or on the opposite do > you feel this would be an opportunity to show something interesting ? No - keep is as simple as possible (but not simpler...). > * If Success (as return by Search) is False then Position is not =A0 > guaranteed to mean anything, simply because in such a circumstance, no = =A0 > postcondition about it applies. I did this way, because I do not know a = =A0 > way to explicitly state =93This is undefined=94. Do you know a better way= to =A0 > express it ? (I could have used a discriminated type for that purpose, bu= t =A0 > SPARK disallow this... as you know). Strengthening the postcondition is a good idea, and one I've followed up on, see below... > > Oops, as last question: I did not understood why, once a time, POGS =A0 > returns me two reports for the same single Run_Test procedure, one which = =A0 > was saying OK and one which I think you might get this if you get a syntax error from the Examiner when generating VCs. I decided that it would more interesting to strengthen the post- condition to say that 'not Success' means that no element in Source is equal to Item. Since this can't be proved without using user rules, I got rid of the checks for the 'div' calculations and added two rules for these as well. I had to introduce a precondition that the Source array is ordered, otherwise the rules wouldn't work. (This leaves an unproven VC in Run_Search, but I don't think this is a big issue.) This is getting a bit too big to post, so the code and user rules are in http://www.sparksure.com/resources/Rosetta_Binary_Search.txt Cheers, Phil