package inv3;

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 == true
	//@invariant els.elementType == \type(String)

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

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

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

	public boolean isIn(String s) {
		return getIndex(s) >= 0;
	}

	private int getIndex(String s)
	//@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();
	}
}