SPARK : third example for Roesetta - reviewers welcome

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

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 wrapping,  
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) = Item)) and
       --#    ((Source'Length = 0) -> (Success = 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 := False;
          -- Default status updated on success.
          Position := Index_Type'First;
          -- Default value (required to not a have a data flow error).

          if Source'Length > 0 then
             Lower := Source'First;
             Upper  := Source'Last;
             Terminated := False;

             while not Terminated loop
                Middle := (Lower + Upper) / 2;
                --# assert
                --#    (Lower >= Source'First) and -- See below.
                --#    (Upper <= Source'Last) and -- See below.
                --#    (Middle >= Lower) and -- Prove Middle in  
Source'Range.
                --#    (Middle <= Upper) and -- Prove Middle in  
Source'Range.
                --#    (Success = False); -- For postcondition.
                if Item < Source (Middle) then
                   if Middle = Lower then
                      -- No lower subrange.
                      Terminated := True;
                   else
                      --# check Middle > Lower;
                      -- For the two following proofs.

                      --# check Middle - 1 >= Lower;
                      --# check Lower + Middle - 1 >= Lower * 2;
                      --# check (Lower + Middle - 1) / 2 >= Lower;
                      -- For "Middle >= Lower" in loop assertion.

                      --# check Lower < Middle;
                      --# check Lower + Middle - 1 <= (Middle - 1) * 2;
                      --# check (Lower + Middle - 1) / 2 <= (Middle - 1);
                      -- For "Middle <= Upper" in loop assertion.
                      Upper := Middle - 1;
                      -- Switch to lower half subrange.
                   end if;
                elsif Item > Source (Middle) then
                   if Middle = Upper then
                      -- No upper subrange.
                      Terminated := True;
                   else
                      --# check Middle < Upper;

                      --# check Upper >= Middle + 1;
                      --# check Middle + 1 + Upper >= (Middle + 1) * 2;
                      --# check (Middle + 1 + Upper) / 2 >= (Middle + 1);
                      -- For "Middle >= Lower" in loop assertion.

                      --# check Middle + 1 <= Upper;
                      --# check Middle + 1 + Upper <= Upper * 2;
                      --# check (Middle + 1 + Upper) / 2 <= Upper;
                      -- For "Middle <= Upper" in loop assertion.
                      Lower := Middle + 1;
                      -- Switch to upper half subrange.
                   end if;
                else
                   -- Found.
                   Success := True;
                   Position := Middle;
                   Terminated := 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  => SPARK_IO.Standard_Output,
          Item  => "Searching for ",
          Stop  => 0);
       SPARK_IO.Put_Integer
         (File  => SPARK_IO.Standard_Output,
          Item  => Item,
          Width => 3,
          Base  => 10);

       SPARK_IO.Put_String
         (File  => SPARK_IO.Standard_Output,
          Item  => " in (",
          Stop  => 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  => SPARK_IO.Standard_Output,
             Item  => Source_Index,
             Width => 3,
             Base  => 10);
       end loop;

       SPARK_IO.Put_String
         (File  => SPARK_IO.Standard_Output,
          Item  => "): ",
          Stop  => 0);
       -- Close list.

       Binary_Searchs.Search
         (Source   => Source,    -- in
          Item     => Item,      -- in
          Success  => Success,   -- out
          Position => Position); -- out

       case Success is
          when True =>
             SPARK_IO.Put_String
               (File  => SPARK_IO.Standard_Output,
                Item  => "found as #",
                Stop  => 0);
             SPARK_IO.Put_Integer
               (File  => SPARK_IO.Standard_Output,
                Item  => Position,
                Width => 0, -- Zero, to stick to the sibling '#' sign.
                Base  => 10);
             SPARK_IO.Put_Line
               (File  => SPARK_IO.Standard_Output,
                Item  => ".",
                Stop  => 0);
          when False =>
             SPARK_IO.Put_Line
               (File  => SPARK_IO.Standard_Output,
                Item  => "not found.",
                Stop  => 0);
       end case;
    end Run_Search;

begin
    SPARK_IO.New_Line (File => SPARK_IO.Standard_Output, Spacing => 1);
    Run_Search (Source => Array_Type'(0, 1, 2, 3, 4), Item => 3);
    Run_Search (Source => Array_Type'(1, 2, 3, 4, 5), Item => 3);
    Run_Search (Source => Array_Type'(1, 2, 3, 4, 5), Item => 0);
    Run_Search (Source => Array_Type'(1, 2, 3, 4, 5), Item => 6);
    Run_Search (Source => Array_Type'(1, 2, 3, 4, 5), Item => 1);
    Run_Search (Source => Array_Type'(1, 2, 3, 4, 5), Item => 5);
    Run_Search (Source => Array_Type'(1, 2, 3, 4, 5), Item => 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 terminates  
(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 “This is undefined”. Do you know a better way to  
express it ? (I could have used a discriminated type for that purpose, but  
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 SIV  
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.