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;
   }
}