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.0 required=5.0 tests=BAYES_00,FILL_THIS_FORM, FILL_THIS_FORM_LOAN,FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,6d79efdb8dde2c5a,start X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,UTF8 Path: g2news1.google.com!news4.google.com!feeder.news-service.com!feeder.news-service.com!de-l.enfer-du-nord.net!feeder1.enfer-du-nord.net!gegeweb.org!aioe.org!not-for-mail From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= Newsgroups: comp.lang.ada Subject: SPARK : third example for Roesetta - reviewers welcome Date: Sun, 15 Aug 2010 08:17:29 +0200 Organization: Ada At Home Message-ID: NNTP-Posting-Host: vW41ugf3bPGxhjQJ6q2hXA.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:13321 Date: 2010-08-15T08:17:29+02:00 List-Id: Hello, Here is about the third example for Rosetta Code () In order to avoid silly error which have bad consequence on SPARK = reputation, as for the first two ones, I assume this may be better to = submit it to interested reviewer. Now I choosed the one about dicho-search (binary-search). http://rosettacode.org/wiki/Binary_search I found this one interesting because 1) it has both a recursive and an = iterative version (the one I prefer) and as SPARK does not support = recursion, I felt this was funny to still be able to overcome this = limitation here with iterative form and show an example of this. 2) This= = was the opportunity to post an example with loop assertion, which is a = main topic in SPARK. 3) Last but not least, this task was many order of = = magnitude easier than the one to prove A * B will not overflow (see = previous topic in this area). Here is the one I came to, with questions also for this one : (for users of GoogleGroups, hope there will not be too much line wrappin= g, = do not remember the line width there) with SPARK_IO; --# inherit SPARK_IO; --# main_program; procedure Program --# global in out --# SPARK_IO.Outputs; --# derives --# SPARK_IO.Outputs from --# SPARK_IO.Outputs; is package Binary_Searchs is subtype Item_Type is Integer; -- From specs. subtype Index_Type is Integer range 1 .. 100; -- Arbitrary limits= . type Array_Type is array (Index_Type range <>) of Item_Type; procedure Search (Source : in Array_Type; Item : in Item_Type; Success : out Boolean; Position : out Index_Type); --# derives --# Success, Position from --# Source, Item; --# post --# (Success -> (Source (Position) =3D Item)) and --# ((Source'Length =3D 0) -> (Success =3D False)); -- If Success is False, nothing can be said about Position. end Binary_Searchs; subtype Index_Type is Binary_Searchs.Index_Type range 1 .. 5; -- Needed to defined constrained Array_Type. subtype Array_Type is Binary_Searchs.Array_Type (Index_Type); -- Needed to pass an array literal to Run_Search (later defined). -- SPARK does not allow an unconstrained type mark for that purpose.= package body Binary_Searchs is procedure Search (Source : in Array_Type; Item : in Item_Type; Success : out Boolean; Position : out Index_Type) is Lower : Index_Type; -- Lower bound of Subrange. Upper : Index_Type; -- Upper bound of Subrange. Middle : Index_Type; -- Position where Item is tested for.= Terminated : Boolean; begin Success :=3D False; -- Default status updated on success. Position :=3D Index_Type'First; -- Default value (required to not a have a data flow error). if Source'Length > 0 then Lower :=3D Source'First; Upper :=3D Source'Last; Terminated :=3D False; while not Terminated loop Middle :=3D (Lower + Upper) / 2; --# assert --# (Lower >=3D Source'First) and -- See below. --# (Upper <=3D Source'Last) and -- See below. --# (Middle >=3D Lower) and -- Prove Middle in = Source'Range. --# (Middle <=3D Upper) and -- Prove Middle in = Source'Range. --# (Success =3D False); -- For postcondition. if Item < Source (Middle) then if Middle =3D Lower then -- No lower subrange. Terminated :=3D True; else --# check Middle > Lower; -- For the two following proofs. --# check Middle - 1 >=3D Lower; --# check Lower + Middle - 1 >=3D Lower * 2; --# check (Lower + Middle - 1) / 2 >=3D Lower; -- For "Middle >=3D Lower" in loop assertion. --# check Lower < Middle; --# check Lower + Middle - 1 <=3D (Middle - 1) * 2= ; --# check (Lower + Middle - 1) / 2 <=3D (Middle - = 1); -- For "Middle <=3D Upper" in loop assertion. Upper :=3D Middle - 1; -- Switch to lower half subrange. end if; elsif Item > Source (Middle) then if Middle =3D Upper then -- No upper subrange. Terminated :=3D True; else --# check Middle < Upper; --# check Upper >=3D Middle + 1; --# check Middle + 1 + Upper >=3D (Middle + 1) * 2= ; --# check (Middle + 1 + Upper) / 2 >=3D (Middle + = 1); -- For "Middle >=3D Lower" in loop assertion. --# check Middle + 1 <=3D Upper; --# check Middle + 1 + Upper <=3D Upper * 2; --# check (Middle + 1 + Upper) / 2 <=3D Upper; -- For "Middle <=3D Upper" in loop assertion. Lower :=3D Middle + 1; -- Switch to upper half subrange. end if; else -- Found. Success :=3D True; Position :=3D Middle; Terminated :=3D True; end if; end loop; end if; end Search; end Binary_Searchs; procedure Run_Search (Source : in Binary_Searchs.Array_Type; Item : in Binary_Searchs.Item_Type) --# global in out --# SPARK_IO.Outputs; --# derives --# SPARK_IO.Outputs from --# SPARK_IO.Outputs, Source, Item; is Success : Boolean; Position : Binary_Searchs.Index_Type; begin SPARK_IO.Put_String (File =3D> SPARK_IO.Standard_Output, Item =3D> "Searching for ", Stop =3D> 0); SPARK_IO.Put_Integer (File =3D> SPARK_IO.Standard_Output, Item =3D> Item, Width =3D> 3, Base =3D> 10); SPARK_IO.Put_String (File =3D> SPARK_IO.Standard_Output, Item =3D> " in (", Stop =3D> 0); -- Open list. for Source_Index in Binary_Searchs.Index_Type range Source'Range loop --# assert True; -- No need for an assertion on anything. SPARK_IO.Put_Integer (File =3D> SPARK_IO.Standard_Output, Item =3D> Source_Index, Width =3D> 3, Base =3D> 10); end loop; SPARK_IO.Put_String (File =3D> SPARK_IO.Standard_Output, Item =3D> "): ", Stop =3D> 0); -- Close list. Binary_Searchs.Search (Source =3D> Source, -- in Item =3D> Item, -- in Success =3D> Success, -- out Position =3D> Position); -- out case Success is when True =3D> SPARK_IO.Put_String (File =3D> SPARK_IO.Standard_Output, Item =3D> "found as #", Stop =3D> 0); SPARK_IO.Put_Integer (File =3D> SPARK_IO.Standard_Output, Item =3D> Position, Width =3D> 0, -- Zero, to stick to the sibling '#' sign.= Base =3D> 10); SPARK_IO.Put_Line (File =3D> SPARK_IO.Standard_Output, Item =3D> ".", Stop =3D> 0); when False =3D> SPARK_IO.Put_Line (File =3D> SPARK_IO.Standard_Output, Item =3D> "not found.", Stop =3D> 0); end case; end Run_Search; begin SPARK_IO.New_Line (File =3D> SPARK_IO.Standard_Output, Spacing =3D> = 1); Run_Search (Source =3D> Array_Type'(0, 1, 2, 3, 4), Item =3D> 3); Run_Search (Source =3D> Array_Type'(1, 2, 3, 4, 5), Item =3D> 3); Run_Search (Source =3D> Array_Type'(1, 2, 3, 4, 5), Item =3D> 0); Run_Search (Source =3D> Array_Type'(1, 2, 3, 4, 5), Item =3D> 6); Run_Search (Source =3D> Array_Type'(1, 2, 3, 4, 5), Item =3D> 1); Run_Search (Source =3D> Array_Type'(1, 2, 3, 4, 5), Item =3D> 5); Run_Search (Source =3D> Array_Type'(1, 2, 3, 4, 5), Item =3D> 2); end Program; Time for questions : * 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 ? * In the loop inside of Search there are Check annotations which was not= = strictly needed but which I still left for more expressiveness. Is that = OK = ? Not too much ? * 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 subrange = width always decrease, so that the loop always terminates. Should I or = should I not get it back ? * I also though about an indirect way to prove the loop always terminate= s = (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 ? * If Success (as return by Search) is False then Position is not = guaranteed to mean anything, simply because in such a circumstance, no = 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 know= a better way to = express it ? (I could have used a discriminated type for that purpose, b= ut = SPARK disallow this... as you know). 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 was saying False. As there can be only one S= IV = file in a given directory, this seemed strange to me. How did he get to = = these two different reports at the same time about a single procedure ? = Do = you know this issue ? I removed all files, this had been sufficient to = solve the trick.