Differences
This shows you the differences between two versions of the page.
— |
treeinsertion.java [2010/05/25 10:48] (current) vkuncak created |
||
---|---|---|---|
Line 1: | Line 1: | ||
+ | <code java> | ||
+ | public class Tree | ||
+ | { | ||
+ | private static Node root; | ||
+ | |||
+ | /*: public static specvar content :: objset; | ||
+ | private vardefs "content == | ||
+ | {x. rtrancl_pt (% x y. x..Node.left = y | x..Node.right = y) root x}"; | ||
+ | |||
+ | invariant "tree [Node.left, Node.right]"; | ||
+ | |||
+ | invariant "root = null | (ALL n. n..Node.left ~= root & n..Node.right ~= root)"; | ||
+ | |||
+ | invariant "ALL x y. x ~= null & y ~= null & (x..Node.right = y | x..Node.left = y) --> y : content"; | ||
+ | |||
+ | invariant "ALL x y. Node.parent x = y --> | ||
+ | (x ~= null & (EX z. z..Node.left = x | z..Node.right = x) --> (y..Node.left = x | y..Node.right = x)) | ||
+ | & (x = null | (ALL z. z..Node.left ~= x & z..Node.right ~= x) --> y = null)"; | ||
+ | |||
+ | */ | ||
+ | | ||
+ | public static void add(Node e, int v) | ||
+ | /*: | ||
+ | requires "e ~: content" | ||
+ | modifies content | ||
+ | ensures "content = old content Un {e}"; | ||
+ | */ | ||
+ | { | ||
+ | Node n = root, p = null; | ||
+ | boolean wentLeft = false; | ||
+ | while (n != null) { | ||
+ | p = n; | ||
+ | if (v < n.v) { | ||
+ | wentLeft = true; | ||
+ | n = n.left; | ||
+ | } else { | ||
+ | wentLeft = false; | ||
+ | n = n.right; | ||
+ | } | ||
+ | } | ||
+ | e.v = v; | ||
+ | if (p == null) { | ||
+ | root = e; | ||
+ | } else { | ||
+ | e.parent = p; | ||
+ | if (wentLeft) { | ||
+ | p.left = e; | ||
+ | } else { | ||
+ | p.right = e; | ||
+ | } | ||
+ | } | ||
+ | } | ||
+ | </code> | ||