gnatprove_13.2.1_28fc3583/share/examples/spark/spark_book/Chapter-07/interval_trees.ads

 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
private with Ada.Finalization;
package Interval_Trees
   with SPARK_Mode => On
is
   type Interval is
      record
         Low  : Float;
         High : Float;
      end record;

   type Tree is limited private;

   -- Inserts Item into tree T.
   procedure Insert (T : in out Tree; Item : in Interval)
     with Global => null,
          Depends => (T => (T, Item));

   function Size (T : in Tree) return Natural
     with Global => null;

private
   pragma SPARK_Mode (Off);

   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;

   type Tree is new Ada.Finalization.Limited_Controlled with
      record
         Root  : Tree_Node_Access := null;
         Count : Natural := 0;
      end record;

   overriding procedure Finalize (T : in out Tree);

end Interval_Trees;