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,ASCII Path: g2news1.google.com!news3.google.com!proxad.net!feeder1-2.proxad.net!news.mixmin.net!aioe.org!not-for-mail From: =?iso-8859-15?Q?Yannick_Duch=EAne_=28Hibou57=29?= Newsgroups: comp.lang.ada Subject: Re: SPARK : third example for Roesetta - reviewers welcome Date: Sun, 15 Aug 2010 22:19:39 +0200 Organization: Ada At Home Message-ID: References: <87aaonlk1h.fsf@hugsarin.sparre-andersen.dk> NNTP-Posting-Host: RZkTY5NyuNCeyE5VNfPAfQ.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-15; 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:13362 Date: 2010-08-15T22:19:39+02:00 List-Id: Hello Jacob :) So you join us too ? This place is starting to be cool. Le Sun, 15 Aug 2010 22:04:26 +0200, Jacob Sparre Andersen = a =E9crit: >> http://rosettacode.org/wiki/Binary_search > >> subtype Item_Type is Integer; -- From specs. > > No need to introduce a subtype here. Just use "Integer" as the elemen= t > type, or introduce a new type with explicit ranges (just to show how > easy it is). The idea was to give a proper name expressing a purpose (I like to start= = to name thing). Well, your idea of "show how easy it is" could be balanced. However, I = have not clear idea about it. Would be nice to know how it is perceived.= = On the other hand, if the purpose of the sorted list is to be general = purpose or even more, precisely to sort Integer, namely, this could be = indeed an option. May be Phil or Jeffrey will have something to state here. >> subtype Index_Type is Integer range 1 .. 100; -- Arbitrary limi= ts. > > Is there really any need to make this a subtype of Integer? Shouldn't= > it rather be a completely independent type: > > type Index_Type is range 1 .. 100; This was rightly to simplify thing (I say "rightly", because you moved i= t = in front above). This was avoiding the need to have some conversion to Integer. > Shouldn't the preconditions include that Source is ordered? That was a topic indeed. Phil and I talked about it in this same thread.= I = first had the idea to express it, but later removed it. > (How do you write that in SPARK?) I did it this way (before I removed it): --# pre --# (Source'Length =3D 0) or else --# (for all I in Index_Type range Source'First .. Source'Last - = 1 --# =3D> (Source (I) <=3D Source (I + 1))); -- The array must be either empty or sorted from lower to higher. Phil did it another way (using an abstract function, if that is the good= = word, i am not sure about the proper way to name it). > The procedure Search should be placed in a package of its own (in theo= ry > it is reusable), and the demonstration program should be a library lev= el > procedure. There is no reason to make the example code more complicat= ed > than that. Yes, that was silly after all. I will split it into proper spec, body an= d = program, this is indeed strongly advised to expose a good example. You a= re = right. I did it this way because I always write test program in a single= = file (and thus declaring package spec and body in the declarative part o= f = the main procedure). Will change it later when I will be finished with = reading Phil's version of the implementation and specs.