Re: SPARK : third example for Roesetta - reviewers welcome

[Jacob Sparre Andersen <sparre@nbi.dk>]

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"