gnatprove_13.2.1_28fc3583/share/examples/spark/spark_book/Chapter-07/interval_tree.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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
with Ada.Unchecked_Deallocation;
package body Interval_Tree
   with
      SPARK_Mode => Off
is
   type Tree_Node;
   type Tree_Node_Access is access Tree_Node;
   type Tree_Node is
      record
         Data        : Interval;
         Maximum     : Float;
         Parent      : Tree_Node_Access := null;
         Left_Child  : Tree_Node_Access := null;
         Right_Child : Tree_Node_Access := null;
      end record;

   -- Intantiate a procedure for deallocating node memory
   procedure Deallocate_Node is new Ada.Unchecked_Deallocation
                                       (Object => Tree_Node,
                                        Name   => Tree_Node_Access);
   type Tree is
      record
         Root  : Tree_Node_Access := null;
         Count : Natural := 0;
      end record;

   T : Tree;  -- The actual tree in this variable package

   procedure Insert (Item : in Interval) is
      New_Node : Tree_Node_Access; -- local to Insert, global to Subtree_Insert

      procedure Subtree_Insert (Pointer : in not null Tree_Node_Access) is
      begin
         if Item.Low <= Pointer.Data.Low then
            if Pointer.Left_Child = null then
               Pointer.Left_Child := New_Node;
               New_Node.Parent := Pointer;
            else
               Subtree_Insert (Pointer.Left_Child);
               Pointer.Maximum :=
                 Float'Max (Pointer.Maximum, Pointer.Left_Child.Maximum);
            end if;
         else
            if Pointer.Right_Child = null then
               Pointer.Right_Child := New_Node;
               New_Node.Parent := Pointer;
            else
               Subtree_Insert (Pointer.Right_Child);
               Pointer.Maximum :=
                 Float'Max (Pointer.Maximum, Pointer.Right_Child.Maximum);
            end if;
         end if;
      end Subtree_Insert;

   begin
      New_Node := new Tree_Node'(Data    => Item,
                                 Maximum => Item.High,
                                 others  => <>);
      if T.Root = null then
         T.Root := New_Node;
      else
         Subtree_Insert (T.Root);
      end if;
      T.Count := T.Count + 1;
   end Insert;


   function Size return Natural is
   begin
      return T.Count;
   end Size;

   procedure Destroy is

      procedure Deallocate_Subtree (Pointer : in out Tree_Node_Access) is
      begin
         if Pointer /= null then
            Deallocate_Subtree (Pointer.Left_Child);
            Deallocate_Subtree (Pointer.Right_Child);
            Deallocate_Node (Pointer);
         end if;
      end Deallocate_Subtree;

   begin
      Deallocate_Subtree (T.Root);
      T.Count := 0;
   end Destroy;

end Interval_Tree;