Re: SPARK code samples

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

Le Wed, 11 Aug 2010 19:33:48 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:
> http://rosettacode.org/wiki/Category:Programming_Tasks
>
> (the first 200 (:-))
>
> Pick any you wish.
Ok. I choose a first one, the one named A+B:
http://rosettacode.org/wiki/A%2BB#Ada

I felt it was interesting because it deals with a case of simple I/O,  
which is a first-time issue with SPARK, and because there was the  
opportunity to expose a simple case of validity check.

However, I don't want to post it there straight away, as I came to two  
dirty questions. First the implementation I end up with, then the two  
questions.


--------------------------------------------------------------------

with SPARK_IO;
--# inherit SPARK_IO;

--# main_program;

procedure A_Plus_B
--# global in out
--#    SPARK_IO.Inputs,
--#    SPARK_IO.Outputs;
--# derives
--#    SPARK_IO.Inputs from
--#       SPARK_IO.Inputs &
--#    SPARK_IO.Outputs from
--#       SPARK_IO.Inputs,
--#       SPARK_IO.Outputs;
is
    A   : Integer;
    B   : Integer;
    Sum : Integer;

    Process_Is_Valid : Boolean;
    Input_Is_OK      : Boolean;
    A_And_B_Sumable  : Boolean;

begin
    Process_Is_Valid := True;

    -- Attempt to Read A from Standard Input.

    SPARK_IO.Get_Integer
      (File  => SPARK_IO.Standard_Input,
       Item  => A,
       Width => 0,
       Read  => Input_Is_OK);

    if not Input_Is_Ok then
       Process_Is_Valid := False;
    end if;

    -- Attempt to Read B from Standard Input.

    B := 0;

    if Process_Is_Valid then
       SPARK_IO.Get_Integer
         (File  => SPARK_IO.Standard_Input,
          Item  => B,
          Width => 0,
          Read  => Input_Is_OK);

       if not Input_Is_Ok then
          Process_Is_Valid := False;
       end if;
    end if;

    -- Get A + B checking the sum is valid in the while.

    Sum := 0;

    if Process_Is_Valid then
       A_And_B_Sumable := False;

       if A >= 0 and B >= 0 then
          if (Integer'Last - A) >= B then
             Sum := A + B;
             A_And_B_Sumable := True;
          end if;
       elsif A >= 0 and B < 0 then
          -- Always valid as the sum is
          -- in range A..B
          Sum := A + B;
          A_And_B_Sumable := True;
       elsif A < 0 and B >= 0 then
          -- Always valid as the sum is
          -- in range A..B
          Sum := A + B;
          A_And_B_Sumable := True;
       elsif A < 0 and B < 0 then
          if (Integer'First - A) <= B then
             Sum := A + B;
             A_And_B_Sumable := True;
          end if;
       end if;

       if not A_And_B_Sumable then
          Process_Is_Valid := False;
       end if;
    end if;

    -- Write A + B.

    if Process_Is_Valid then
       SPARK_IO.Put_Integer
         (File  => SPARK_IO.Standard_Output,
          Item  => Sum,
          Width => 0,
          Base  => 10);
    else
       SPARK_IO.Put_Line
         (File => SPARK_IO.Standard_Output,
          Item => "Either the input or the sum was invalid.",
          Stop => 0); -- 0 means no extra spaces will be written.
    end if;

end A_Plus_B;

--------------------------------------------------------------------


Questions:

* The page says the input of both A and B is supposed to be in range  
-1000..+1000. Obviously there is no way to assert this, so I simply  
dropped the assumption. Are you OK ?

* I could have made a test to ensure inputs of A and B is in -1000..+1000,  
while this would not avoid the need to check for the sum validity, as  
formally speaking there is no way to assert anything on Integer range.  
Second reason to dropped this assumption. OK ?

This case apart, I was thinking giving SPARK examples there, we may not  
rely on user defined rules nor on the checker. Things should be provable  
as-is.


-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.