--
--  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;
         Parent : access Node_Type;
         Right, Left : access Node_Type;
      end record;
end RB_Tree;