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=ham 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,UTF8 Path: g2news1.google.com!news4.google.com!feeder2.cambriumusenet.nl!feed.tweaknews.nl!192.87.166.28.MISMATCH!tudelft.nl!txtfeed1.tudelft.nl!zen.net.uk!dedekind.zen.co.uk!aioe.org!not-for-mail From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= Newsgroups: comp.lang.ada Subject: Re: SPARK : third example for Roesetta - reviewers welcome Date: Sun, 15 Aug 2010 21:32:16 +0200 Organization: Ada At Home Message-ID: References: <589eea9a-0b14-4ae5-bf62-9abf4b33e7fb@i31g2000yqm.googlegroups.com> NNTP-Posting-Host: RZkTY5NyuNCeyE5VNfPAfQ.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes Content-Transfer-Encoding: Quoted-Printable X-Complaints-To: abuse@aioe.org X-Notice: Filtered by postfilter v. 0.8.2 User-Agent: Opera Mail/10.61 (Win32) Xref: g2news1.google.com comp.lang.ada:13357 Date: 2010-08-15T21:32:16+02:00 List-Id: Le Sun, 15 Aug 2010 20:42:27 +0200, Phil Thornley = a =C3=A9crit: > >> 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. I see the point. I though about this one first and then changed my mind,= = may be for two bad reasons (will have to be checked) : first may be I di= d = useless "optimization" (do not know how good compilers handle this), and= = then, I though this may be better if ever the context may have some kind= = of tasking. About the latter, I will have to check if weither or not an = = out value is supposed to be updated only when the method exit or is = possibly updated outside while the method is running. >> 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. I was wondering about reader which may try the example as-is. As was = "afraid" to think someone may try it and see that "unexpected" message = from the Examiner. Or may be there is a place some kind of more = useful-looking assertion here instead of a dummy one ? OTH, while I thinking about your comment, I cannot avoid this though: = after all, if a loop assertion is really missing, this inevitably ends u= p = into undischarged Validation Conditions. So in some sense, this warning = is = useless, because 1) when it is meaningful, it is redundant with later = reports of undischarged VC 2) if this does not ends into undischarged VC= , = this is not meaningful. So, this is either not meaningful either = redundant. May be this is disabled by default in the Examiner's builtin = = options ? ... I still wonder about readers who may get this warning without this. = = But for Real Use, I agree with you, the idea of disabling this warning i= s = indeed good. >> SPARK_IO.Put_Integer >> (File =3D> SPARK_IO.Standard_Output, >> Item =3D> Source_Index, > This line just prints the index - should be Item =3D> > Source(Source_Index), Don't mind for this one Phil, this was a transient modification which = occurs at the same time I was posting this here (I did both thing at the= = time and did not notice I was posting an error). The one at Rosetta do = Source (Source_Index); it was corrected in the afternoon (local time, lo= l). >> 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. Mmmh, your informal argument makes me think this may be matter of taste = = this one, both for case and name. However, will think about it. Well, yo= u = may be right for Success vs Found ; will change it ; except for Case = Statement which I do not wish to change for the time. I have reasons for= = that, but don't want to argue about it here (to not obfuscate the topic,= = ... will just say, to keep it simple, I don't enjoy the =E2=80=9Celse=E2= =80=9D branches of = "if-then" constructs... I call it =E2=80=9Cthe mute branch=E2=80=9D). >> * The test part, that is Run_Search and body of Program takes up to = >> half 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. OK. As there was a doubt in my mind about it, I added a comment suggesti= ng = to focus only on the relevant part. So I may remove it. Will have this i= n = mind for future example. >> * In the loop inside of Search there are Check annotations which was = = >> not strictly needed but which I still left for more expressiveness. I= s = >> that OK ? Not too much ? > I prefer user rules to large numbers of check annotations, but YMMV. I don't want to introduce user rules at Rosetta, because don't think thi= s = is the place for such none-straight-way things. About Real Use, this is another topic. >> * To keep it simple so far, I have dropped a precondition which I = >> initially started with and which was requiring the array to be sorted= . = >> This only impact semantic, not runtime check, as any way, the subrang= e = >> width always decrease, so that the loop always terminates. Should I o= r = >> should I not get it back ? > See my version below (which requires this precondition). OK. Will see right after (I reply as I read) >> * I also though about an indirect way to prove the loop always = >> terminates >> (although this is not a feature supported by SPARK, there are indirec= t >> ways to achieve this). I though this would look like too much obfusca= ted >> 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 = >> guaranteed to mean anything, simply because in such a circumstance, n= o = >> postcondition about it applies. I did this way, because I do not know= a = >> way to explicitly state =E2=80=9CThis is undefined=E2=80=9D. Do you k= now a better way = >> to express it ? (I could have used a discriminated type for that = >> purpose, but 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 = >> returns me two reports for the same single Run_Test procedure, one = >> which was saying OK and one which > I think you might get this if you get a syntax error from the Examiner= > when generating VCs. And this could end into two SIV files in the same folder for the same = procedure ? > 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. May be I see. This suggest the most typical or expected result is Found,= = instead of not Found, and so you are focusing on the consequence of not = = Found, which are more likely to need care. > 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 OK. The cool stuff to read is there :) I enjoy your contribution, with the one of Jeffrey too. I was pleased. Well, well, now time to read your version. "See" you soon. -- = There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise.