Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- --
- -- 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;
- --
- -- 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;
- Parent : access Node_Type := null;
- Right, Left : access Node_Type := null;
- end record;
- end RB_Tree;
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement