import java.util.Vector;

// Based on IntSet From Liskov and Guttag, Figure 5.6.

public class StringSet {
    // OVERVIEW: StringSets are unbounded, mutable sets of Strings.
    //    A typical StringSet is {x1, ..., xn}
    
    // Representation:
    private Vector els;

    // AF(c) = { c.els[i] | 0 <= i <= c.els.size }
    // RI(c) = c.els != null && 
    //         for all integers i . c.els[i] is a String &&
    //         there are no duplicates in c.els

    //@invariant els != null
    //@invariant els.containsNull == false
    //@invariant els.elementType == \type(String)

    public StringSet () {
	// EFFECTS: Initializes this to be empty: { }
	els = new Vector ();
	//@set els.elementType = \type(String)
	//@set els.containsNull = false
    }  // ESC/Java is unable to prove the invariant for the empty constructor without the set's.

    public void insert (String s) 
        //@requires s != null
    {
	// MODIFIES: this
	// EFFECTS: Adds x to the elements of this.
	if (getIndex (s) < 0) els.add (s); 
    }

    public void remove (String s) 
        //@requires s != null
    {
	// MODIFIES: this
	// EFFECTS: Removes s from this.
	int i = getIndex (s);
	if (i < 0) return;
	els.removeElementAt (i);
    }
	
    public boolean isIn (String s) 
        //@requires s != null
    {
	return getIndex (s) >= 0;
    }

    private int getIndex (String s) 
        //@requires s != null
        //@ensures \result < els.elementCount
    {
	// EFFECTS: If x is in this returns index where x appears, else returns -1.
	for (int i = 0; i < els.size (); i++) {
	    if (s == null) {
		if (els.elementAt (i) == null) {
		    return i;
		}
	    } else {
		if (s.equals (els.elementAt (i))) {
		    return i;
		}
	    }
	}
	
	return -1;
    }

    public int size () {
	// EFFECTS: Returns the number of elements in this.
	return els.size ();
    }
}