--
--  Copyright (c) 2010, Edward O'Callaghan
--
--  Permission to use, copy, modify, and/or distribute this software for any
--  purpose with or without fee is hereby granted, provided that the above
--  copyright notice and this permission notice appear in all copies.
--
--  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
--  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
--  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
--  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
--  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
--  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
--  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
--

--
--  SPARK Verified Ada2005 Red-Back Tree in-memory implementation.

generic
   type Element_Type is private;

package RB_Tree is
   type Node_Type is tagged limited private;

   type disk_Node_Type   is new Node_Type with private;
   type memory_Node_Type is new Node_Type with private;

   --
   --  Red-Black Tree Insertion
   -- Time Complexity:
   -- Average Case: O( Log[N] )
   -- Worst Case: O( Log[N] )
   procedure Insert (Tree : in out Node_Type; Element : in Element_Type);
   --# derives Tree from *, Element;

   --
   --  Red-Black Tree Deletion
   -- Time Complexity:
   -- Average Case: O( Log[N] )
   -- Worst Case: O( Log[N] )
   procedure Delete (Tree : in out Node_Type; Node : in Node_Type);
   --# derives Tree from *, Node;

   --
   --  Red-Black Tree Search
   -- Time Complexity:
   -- Average Case: O( Log[N] )
   -- Worst Case: O( Log[N] )
   procedure Search
     (Tree    : in Node_Type;
      Element : in Element_Type;
      Found   : out Boolean;
      Node    : out Node_Type);
   --# derives Found, Node from
   --#  Tree, Element;
   --# post Found -> Tree (Node) = Element;
   --  If Found is False then Node is undefined.

private
   type Node_Colour is (Red, Black);

   type Node_Type is record
      Colour : Node_Colour := Black;
   end record;


   type disk_Node_Type   is new Node_Type with
      record
         Parent      : access disk_Node_Type := null;
         Right, Left : access disk_Node_Type := null;
      end record;

   type memory_Node_Type   is new Node_Type with
      record
         Parent      : access memory_Node_Type := null;
         Right, Left : access memory_Node_Type := null;
      end record;

end RB_Tree;