import org.jmlspecs.models.JMLValueToObjectMap;

public class Map {
    class Node {
	Key key;
	Object value;
	Node left, right;
	
	Node(Key k, Object v, Node l, Node r) {
	    key = k;
	    value = v;
	    left = l;
	    right = r;
	}
    }
    
    private /*@ spec_public nullable @*/ Node root;
    
    /*@ private model pure JMLValueToObjectMap computeContent(Node n) {
      TODO: Implement
      }
    */


    /*@ public model JMLValueToObjectMap content; */
    /*@ private represents content <- computeContent(root); */

    /*@ TODO: Specify */
    public Object add(Key k, Object v) { 
	// TODO: Implement
    }

    /*@ TODO: Specify */
    public /*@ pure @*/ Object get(Key k) {
	// TODO: Implement
    }

    private /*@ pure @*/ String toStringHelper(/*@ nullable @*/ Node node, String rep0){ 
	if(node == null) return rep0;
	
	String rep = new String(rep0 + (node != root ? ", " : ""));
	return new String(toStringHelper(node.right, toStringHelper(node.left, rep + node.key.toString() + " -> " + node.value.toString()))); 
    }

   
    public /*@ pure @*/ String toString(){
	return new String(toStringHelper(root,"{") + "}");
    }

}