-- By Jacob Sparre Andersen
-- Validates with SPARK GPL 2010's Examiner/Simplifier

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;