Differences

This shows you the differences between two versions of the page.

@@ 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>