--
--  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 generic implementation,
--  provides both  in-memory and on-disk facilities.

--
--  Red-Black Tree Properties:
--
--  1.) A node is either Red or Black, Root node is always Black.
--  2.) All leave nodes are Black.
--  3.) Both children of every Red node are black.
--  4.) Every simple* path from a given node to any of its descendant
--       leaves contains the same number of Black nodes.
--  *A path with no repeated vertices is called a simple path.

generic
   type Element_Type is private;

package ADT.RB_Tree is

   type Node_Type is abstract tagged limited private;

   --
   --  Red-Black Tree Constructor
   function Initialize_Memory_Tree return  Node_Type'Class;
   function Initialize_On_Disk_Tree return  Node_Type'Class;

   --
   --  Red-Black Tree Destructor
   procedure Finalize (Tree : in out Node_Type) is abstract;
   --# derives Tree from *;

   --
   --  Red-Black Tree Insertion
   --  Time Complexity:
   --  Average Case: O( Log[N] )
   --  Worst Case: O( Log[N] )
   procedure Insert
     (Tree    : access Node_Type;
      Element : in Element_Type)
is abstract;
   --# 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)
is abstract;
   --# 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)
is abstract;
   --# 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 abstract tagged limited record
      Colour : Node_Colour := Black;
      --  Parent      : access Node_Type := null;
      --  Right, Left : access Node_Type := null;
   end record;

end ADT.RB_Tree;