--
--  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.

--
--  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
package RB_Tree is

   type Tree_Type is limited private;
   type Node_Type is limited private;

   --
   --  Red-Black Tree Constructor
   procedure Initialize (Tree : in out Tree_Type; Element : in Element_Type);
   --# derives Tree from *, Element;

   --
   --  Red-Black Tree Destructor
   procedure Destroy (Tree : in out Tree_Type);
   --# derives Tree from *;

   --
   --  Red-Black Tree Insertion
   --  Time Complexity:
   --  Average Case: O( Log[N] )
   --  Worst Case: O( Log[N] )
   procedure Insert (Tree : in out Tree_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 Tree_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 Tree_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 Tree_Type is new Node_Type;

   type Node_Type is record
      Colour      : Node_Colour      := Black;
      Parent      : access Node_Type := null;
      Right, Left : access Node_Type := null;
   end record;
end RB_Tree;
--  end ADT.RB_Tree;