Differences
This shows you the differences between two versions of the page.
— |
threadedtree.java [2009/01/30 12:21] (current) wies created |
||
---|---|---|---|
Line 1: | Line 1: | ||
+ | ====== Insertion into a Sorted Threaded Tree ====== | ||
+ | <code java> | ||
+ | public final class Node { | ||
+ | public /*: claimedby Tree */ Node right; | ||
+ | public /*: claimedby Tree */ Node left; | ||
+ | public /*: claimedby Tree */ Node next; | ||
+ | public /*: claimedby Tree */ int v; | ||
+ | } | ||
+ | |||
+ | public class ThreadedTree | ||
+ | { | ||
+ | private static Node root; | ||
+ | private static Node first; | ||
+ | |||
+ | /*: public static specvar content :: objset; | ||
+ | private vardefs "content == | ||
+ | {x. rtrancl_pt (% x y. x..left = y | x..right = y) root x}"; | ||
+ | |||
+ | invariant "tree [left, right]"; | ||
+ | |||
+ | invariant "root ~= null --> (ALL n. n..left ~= root & n..right ~= root)"; | ||
+ | invariant "first ~= null --> (ALL n. n..next ~= first)"; | ||
+ | invariant "(first,root) : {(x,y). x..next = y}^*"; | ||
+ | |||
+ | invariant "ALL x y. x ~= null & y ~= null & (x..right = y | x..left = y) --> y : content"; | ||
+ | invariant "ALL x y. x..next = y <-> | ||
+ | (x ~= null --> | ||
+ | (x..right = null --> | ||
+ | ((EX z. z..left = x) --> y..left = x) & | ||
+ | ((ALL z. z..left ~= x) --> | ||
+ | (((ALL z. (left z, x) ~: {(x1,x2). x1..right = x2}^*)) & (y = null) | | ||
+ | (left y, x) : {(x1,x2). x1..right = x2}^*))) & | ||
+ | (x..right ~= null --> | ||
+ | y..left = null & y ~= null & (right x, y) : {(x1, x2). x1..left = x2}^*)) & | ||
+ | (x = null --> y = null)"; | ||
+ | invariant "ALL x. x : content & x ~= null & x..next ~= null --> x..v <= x..next..v"; | ||
+ | |||
+ | */ | ||
+ | |||
+ | public static void add(Node e) | ||
+ | /*: | ||
+ | requires "e ~: content" | ||
+ | modifies content | ||
+ | ensures "content = old content Un {e}"; | ||
+ | */ | ||
+ | { | ||
+ | Node n = root, p = null; | ||
+ | Node pred = null; | ||
+ | Node succ = null; | ||
+ | boolean wentLeft = false; | ||
+ | while (n != null) { | ||
+ | p = n; | ||
+ | if (e.v < n.v) { | ||
+ | wentLeft = true; | ||
+ | succ = n; | ||
+ | n = n.left; | ||
+ | } else { | ||
+ | wentLeft = false; | ||
+ | pred = n; | ||
+ | n = n.right; | ||
+ | } | ||
+ | } | ||
+ | if (p == null) { | ||
+ | root = e; | ||
+ | } else { | ||
+ | if (wentLeft) { | ||
+ | p.left = e; | ||
+ | } else { | ||
+ | p.right = e; | ||
+ | } | ||
+ | } | ||
+ | e.next = succ; | ||
+ | if (pred != null) pred.next = e; | ||
+ | } | ||
+ | } | ||
+ | </code> |