gnatprove_13.2.1_28fc3583/share/examples/spark/spark_book/Chapter-07/interval_trees.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
with Ada.Unchecked_Deallocation;

package body Interval_Trees
  with SPARK_Mode => Off is

   procedure Deallocate_Node is new
      Ada.Unchecked_Deallocation (Object => Tree_Node, Name => Tree_Node_Access);

   -- Inserts Item into tree T. Duplicate items overwrite existing tree elements.
   procedure Insert (T : in out Tree; Item : in Interval) is
      New_Node : Tree_Node_Access := new Tree_Node'(Data => Item, Maximum => Item.High, others => <>);

      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
      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 (T : in Tree) return Natural is
   begin
      return T.Count;
   end Size;


   procedure Finalize (T : in out Tree) is

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

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

end Interval_Trees;