Differences

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

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