LARA

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