public final class Node {
   public /*: claimedby Tree */ Node right;
   public /*: claimedby Tree */ Node left;
   public /*: claimedby Tree */ Object data;
}
 
public class SizeDataTree
{
   private static Node root;
   private static int size;
   /*: private static specvar inlist :: objset;
       public static specvar content :: objset;
       private vardefs "inlist ==
        {x. rtrancl_pt (% x y. x..Node.left = y | x..Node.right = y) root x}";
 
       private vardefs "content ==
        {x. EX n. n ~= null & n : inlist & n..data = x}"
 
       invariant "tree [Node.left, Node.right]";
 
       invariant "inlist <= Object.alloc";
 
       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 : inlist";
 
       invariant "size = card content";
   */
 
   public static void add(Object e)
      /*:
        requires "e ~: content & e ~= null"
        modifies content
        ensures "content = old content Un {e}";
      */
   {
      Node n = root, p = null;
      boolean wentLeft = false;
      while (n != null) {
         //: havoc "wentLeft";
         p = n;
         if (wentLeft) {
            n = n.left;
         } else {
            n = n.right;
         }
      }
      Node n = new Node();
      n.data = e;
      if (p == null) {
         root = n;
      } else {
         if (wentLeft) {
            p.left = n;
         } else {
            p.right = n;
         }
      }
      size = size + 1;
   }
}