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