gnatprove_13.2.1_28fc3583/share/examples/spark/spark_book/Chapter-02/example.adb

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
with Ada.Text_IO;
with Ada.Integer_Text_IO;
procedure Example with
  Annotate => (GNATprove, Might_Not_Return)
is

   Limit : constant Integer := 1_000;

   procedure Bounded_Increment
     (Value   : in out Integer;  -- A value to increment
      Bound   : in     Integer;  -- The maximum that Value may take
      Changed :    out Boolean)  -- Did Value change?
   is
   begin
      if Value < Bound then
         Value   := Value + 1;
         Changed := True;
      else
         Changed := False;
      end if;
   end Bounded_Increment;

   Value    : Integer;
   Modified : Boolean;

begin -- procedure Example
   Ada.Text_IO.Put_Line ("Enter a number.");
   Ada.Integer_Text_IO.Get (Value);
   Bounded_Increment (Bound   => Limit / 2,
                      Value   => Value,
                      Changed => Modified);
   if Modified then
      Ada.Text_IO.Put_Line ("Your number was changed to ");
      Ada.Integer_Text_IO.Put (Item  => Value,
                                Width => 1);
   end if;
end Example;