Re: SPARK : third example for Roesetta - reviewers welcome

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

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 <sparre@nbi.dk>  
a écrit:
>> 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).
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 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;
This was rightly to simplify thing (I say "rightly", because you moved it  
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 = 0) or else
    --#    (for all I in Index_Type range Source'First .. Source'Last - 1
    --#       => (Source (I) <= 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 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.
Yes, that was silly after all. I will split it into proper spec, body and  
program, this is indeed strongly advised to expose a good example. You are  
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 of  
the main procedure). Will change it later when I will be finished with  
reading Phil's version of the implementation and specs.