ESC/Java version 1.2.4, 27 September 2001

StringSet ...

StringSet: StringSet() ...
------------------------------------------------------------------------
StringSet.java:24: Warning: Possible violation of object invariant (Invariant)
    }
    ^
Associated declaration is "StringSet.java", line 18, col 7:
    //@invariant els.containsNull == true
       ^
Possibly relevant items from the counterexample context:  
  (vAllocTime(brokenObj<4>) < after@21.24-21.24)
  ... (18 lines cut showing counterexample)
  brokenObj<4> != null
(brokenObj* refers to the object for which the invariant is broken.)

------------------------------------------------------------------------
StringSet.java:24: Warning: Possible violation of object invariant (Invariant)
    }
    ^
Associated declaration is "StringSet.java", line 19, col 7:
    //@invariant els.elementType == \type(String)
       ^
Possibly relevant items from the counterexample context:  
  objectToBeConstructed == brokenObj<5>
  RES-21.24:21.24 == brokenObj<5>
(brokenObj* refers to the object for which the invariant is broken.)

------------------------------------------------------------------------
    [0.417 s]  failed

StringSet: insert(java.lang.String) ...
    [0.082 s]  passed

StringSet: remove(java.lang.String) ...
------------------------------------------------------------------------
StringSet.java:37: Warning: Precondition possibly not established (Pre)
        els.removeElementAt (i);
                            ^
Associated declaration is "/net/af10/evans/escjava/escjava/lib/specs/java/util/Vector.spec", line 569, col 8:
    //@ requires index < elementCount ;
        ^
Execution trace information:
    Executed else branch in "StringSet.java", line 36, col 1.

------------------------------------------------------------------------
    [0.158 s]  failed

StringSet: isIn(java.lang.String) ...
    [0.014 s]  passed

StringSet: getIndex(java.lang.String) ...
------------------------------------------------------------------------
StringSet.java:47: Warning: Possible null dereference (Null)
            if (s.equals (els.elementAt (i))) {
                 ^
Execution trace information:
    Reached top of loop after 0 iterations in "StringSet.java", line 46, col 1.

------------------------------------------------------------------------
    [0.173 s]  failed

StringSet: size() ...
    [0.033 s]  passed
  [1.952 s total]
4 warnings