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 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!news4.google.com!proxad.net!feeder1-2.proxad.net!u-picardie.fr!news.ecp.fr!news.jacob-sparre.dk!pnx.dk!not-for-mail
From: Jacob Sparre Andersen <sparre@nbi.dk>
Newsgroups: comp.lang.ada
Subject: Re: SPARK : third example for Roesetta - reviewers welcome
Date: Sun, 15 Aug 2010 22:04:26 +0200
Organization: Jacob Sparre Andersen
Message-ID: <87aaonlk1h.fsf@hugsarin.sparre-andersen.dk>
References: <op.vhguffh3ule2fv@garhos>
NNTP-Posting-Host: 94.191.136.78.bredband.3.dk
Mime-Version: 1.0
Content-Type: text/plain; charset=iso-8859-1
Content-Transfer-Encoding: 8bit
X-Trace: munin.nbi.dk 1281902669 23090 94.191.136.78 (15 Aug 2010 20:04:29
 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Sun, 15 Aug 2010 20:04:29 +0000 (UTC)
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.1 (gnu/linux)
Cancel-Lock: sha1:LWwFH/ZIqUsiXE3QeANxsxRJ664=
Xref: g2news1.google.com comp.lang.ada:13359
Date: 2010-08-15T22:04:26+02:00
List-Id: <comp.lang.ada>

Yannick Duch�ne wrote:

> 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 element
type, or introduce a new type with explicit ranges (just to show how
easy it is).

>       subtype Index_Type is Integer range 1 .. 100; -- Arbitrary limits.

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;

>       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) = Item)) and
>       --#    ((Source'Length = 0) -> (Success = False));
>       -- If Success is False, nothing can be said about Position.

Shouldn't the preconditions include that Source is ordered?  (How do you
write that in SPARK?)

The procedure Search should be placed in a package of its own (in theory
it is reusable), and the demonstration program should be a library level
procedure.  There is no reason to make the example code more complicated
than that.

Greetings,

Jacob
-- 
"... but it was, on the other hand, very good at being a slow
 and dim-witted pupil."
"I had no idea they were supposed to be in short supply"