--
--  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 limited private;

   procedure Insert (Tree : in out Node_Type; Element : in Element_Type);
   --# derives Tree from *, Element;

   procedure Delete (Tree : in out Node_Type; Node : in Node_Type);
   --# derives Tree from *, Node;

   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 Position is undefined.

private
   type Node_Colour is (Red, Black);

   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;