Re: SPARK code samples

["cjpsimon@gmail.com" <cjpsimon@gmail.com>]

On 12 août, 04:39, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> Le Wed, 11 Aug 2010 19:33:48 +0200, Dmitry A. Kazakov  
> <mail...@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 ?
>

The RM : In an implementation, the range of Integer shall include the
range –2**15+1 .. +2**15–1.

> 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.