44 lines
1.1 KiB
Text
44 lines
1.1 KiB
Text
-- 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;
|