Re: SPARK code samples

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

Yannick Duch�ne wrote:

> Ok. I choose a first one, the one named A+B:
> http://rosettacode.org/wiki/A%2BB#Ada

[...]

I think you have made the problem much too complicated.  Isn't this
sufficient?  (I haven't got a SPARK Examiner right here.)

------------------------------------------------------------
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
   subtype Small_Integers is Integer range -1_000 .. +1_000;
   A, B       : Integer;
   A_OK, B_OK : Boolean;
begin
   SPARK_IO.Get_Integer (File  => SPARK_IO.Standard_Input,
                         Item  => A,
                         Width => 0,
                         Read  => A_OK);
   A_OK := A_OK and A in Small_Integers;
   SPARK_IO.Get_Integer (File  => SPARK_IO.Standard_Input,
                         Item  => B,
                         Width => 0,
                         Read  => B_OK);
   B_OK := B_OK and B in Small_Integers;
   if A_OK and B_OK then
      SPARK_IO.Put_Integer (File  => SPARK_IO.Standard_Output,
                            Item  => A + B,
                            Width => 4,
                            Base  => 10);
   else
      SPARK_IO.Put_Line (File => SPARK_IO.Standard_Output,
                         Item => "Input data does not match specification.",
                         Stop => 0);
   end if;
end A_Plus_B;
------------------------------------------------------------

Kind regards,

Jacob Sparre Andersen
--
Jacob Sparre Andersen Research & Innovation
Vesterbrogade 148K, 1. th.
1620 K�benhavn V
Danmark

Phone:    +45 21 49 08 04
E-mail:   jacob@jacob-sparre.dk
Web-site: http://www.jacob-sparre.dk/