Map.java

File contents

import org.jmlspecs.models.JMLValueToObjectMap;
import java.util.NoSuchElementException;

public class Map {
   
    private /*@ spec_public nullable @*/ Node root;

    Map() {
      /*@ set content = computeContent(root); @*/
    }
    
    /*@ private model pure JMLValueToObjectMap computeContent(nullable Node n) {
      TODO: Implement
      }
    */

    /*@ public nullable ghost JMLValueToObjectMap content; */

    /*@ 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,"{") + "}");
    }

}

class Node {
    Key key;
    Object value;
    /*@ nullable @*/ Node left, right;
    
    Node(Key k, Object v,/*@ nullable @*/ Node l,/*@ nullable @*/ Node r) {
        key = k;
        value = v;
        left = l;
        right = r;
    }

}