JML

org.jmlspecs.models
Class JMLObjectSet

java.lang.Object
  extended byorg.jmlspecs.models.JMLObjectSet
All Implemented Interfaces:
Cloneable, JMLCollection, JMLType, Serializable

public class JMLObjectSet
extends Object
implements JMLCollection

Sets of objects. This type uses "==" to compare elements, and does not clone elements that are passed into and returned from the set's methods.

For the purposes of informal specification in the methods below, we assume there is a model field

public model mathematical_set theSet;
that you can think of as a mathematical set of objects.

Version:
$Revision: 1.84 $
Author:
Gary T. Leavens, with help from Albert Baker, Clyde Ruby, and others.
See Also:
JMLCollection, JMLType, JMLEqualsSet, JMLValueSet, JMLObjectSetEnumerator, JMLObjectBag, JMLEqualsBag, JMLValueBag

Class Specifications
public invariant ( \forall org.jmlspecs.models.JMLObjectSet s2; s2 != null; ( \forall java.lang.Object e1, e2; ; equational_theory(this,s2,e1,e2)));
public invariant this.elementType <: \type(java.lang.Object);
public invariant ( \forall java.lang.Object o; o != null&&this.has(o); \typeof(o) <: this.elementType);
public invariant this.containsNull <==> this.has(null);
public invariant_redundantly this.isEmpty() ==> !this.containsNull;
protected invariant this.the_list == null ==> this.size == 0;
protected invariant this.the_list != null ==> this.size == this.the_list.int_size();
protected invariant (this.the_list == null) == (this.size == 0);
protected invariant this.size >= 0;
protected invariant this.the_list != null&&this.the_list.next != null ==> !this.the_list.next.has(this.the_list.val);
protected invariant_redundantly (* the_list has no duplicates *);
protected invariant this.size == 0 ==> !this.containsNull;
public invariant this.owner == null;

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Specifications inherited from interface JMLCollection
instance public constraint this.elementType == \old(this.elementType);
instance public constraint this.containsNull == \old(this.containsNull);

Model Field Summary
 
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
 
Model fields inherited from interface org.jmlspecs.models.JMLCollection
elementState
 
Ghost Field Summary
 
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
 
Ghost fields inherited from interface org.jmlspecs.models.JMLCollection
containsNull, elementType
 
Field Summary
static JMLObjectSet EMPTY
          The empty JMLObjectSet.
[spec_public] protected  int size
          The number of elements in this set.
protected  JMLListObjectNode the_list
          The list representing the elements of this set.
 
Constructor Summary
  JMLObjectSet()
          Initialize this to be an empty set.
  JMLObjectSet(Object e)
          Initialize this to be a singleton set containing the given element.
protected JMLObjectSet(nullable JMLListObjectNode ls)
          Initialize this set with the given list.
protected JMLObjectSet(nullable JMLListObjectNode ls, int sz)
          Initialize this set with the given instance variables.
 
Model Method Summary
static boolean equational_theory(JMLObjectSet s, JMLObjectSet s2, Object e1, Object e2)
          An equational specification of the properties of sets.
 
Model methods inherited from class java.lang.Object
hashValue
 
Model methods inherited from interface org.jmlspecs.models.JMLCollection
size
 
Method Summary
 Object choose()
          Return an arbitrary element of this.
 Object clone()
          Return a clone of this object.
 boolean containsAll(non_null Collection c)
          Tell whether, for each element in the given collection, there is a "==" element in this set.
static JMLObjectSet convertFrom(non_null Object[] a)
          Return the set containing all the elements in the given array.
static JMLObjectSet convertFrom(non_null Collection c)
          Return the set containing all the object in the given collection.
static JMLObjectSet convertFrom(non_null JMLCollection c)
          Return the set containing all the object in the given JMLCollection.
 JMLObjectSet difference(non_null JMLObjectSet s2)
          Returns a new set that contains all the elements that are in this but not in the given argument.
 JMLObjectSetEnumerator elements()
          Returns an Enumeration over this set.
 boolean equals(nullable Object s2)
          Test whether this object's value is equal to the given argument.
protected  JMLObjectSet fast_insert(Object elem)
          Returns a new set that contains all the elements of this and also the given argument, assuming the argument is not in the set.
 boolean has(Object elem)
          Is the argument "==" to one of the objects in theSet.
 int hashCode()
          Return a hash code for this object.
 JMLObjectSet insert(Object elem)
          Returns a new set that contains all the elements of this and also the given argument.
 int int_size()
          Tells the number of elements in the set.
 JMLObjectSet intersection(non_null JMLObjectSet s2)
          Returns a new set that contains all the elements that are in both this and the given argument.
 boolean isEmpty()
          Is the set empty.
 boolean isProperSubset(non_null JMLObjectSet s2)
          Tells whether this set is a subset of but not equal to the argument.
 boolean isProperSuperset(non_null JMLObjectSet s2)
          Tells whether this set is a superset of but not equal to the argument.
 boolean isSubset(non_null JMLObjectSet s2)
          Tells whether this set is a subset of or equal to the argument.
 boolean isSuperset(non_null JMLObjectSet s2)
          Tells whether this set is a superset of or equal to the argument.
 JMLIterator iterator()
          Returns an Iterator over this set.
 JMLObjectSet powerSet()
          Returns a new set that is the set of all subsets of this.
 JMLObjectSet remove(Object elem)
          Returns a new set that contains all the elements of this except for the given argument.
static JMLObjectSet singleton(Object e)
          Return the singleton set containing the given element.
 Object[] toArray()
          Return a new array containing all the elements of this.
 JMLObjectBag toBag()
          Return a new JMLObjectBag containing all the elements of this.
 JMLObjectSequence toSequence()
          Return a new JMLObjectSequence containing all the elements of this.
 String toString()
          Return a string representation of this object.
 JMLObjectSet union(non_null JMLObjectSet s2)
          Returns a new set that contains all the elements that are in either this or the given argument.
 
Methods inherited from class java.lang.Object
finalize, getClass, notify, notifyAll, wait, wait, wait
 

Field Detail

the_list

protected final JMLListObjectNode the_list
The list representing the elements of this set.

Specifications: nullable
is in groups: objectState
maps the_list.elementState \into elementState

size

protected final int size
The number of elements in this set.

Specifications: spec_public
is in groups: objectState

EMPTY

public static final JMLObjectSet EMPTY
The empty JMLObjectSet.

See Also:
JMLObjectSet()
Specifications: non_null
Constructor Detail

JMLObjectSet

public JMLObjectSet()
Initialize this to be an empty set.

See Also:
EMPTY
Specifications: (class)pure
public normal_behavior
assignable objectState, elementType, containsNull, owner;
ensures this.isEmpty();
ensures_redundantly (* this is an empty set *);
    implies_that
ensures this.elementType <: \type(java.lang.Object)&&!this.containsNull;

JMLObjectSet

public JMLObjectSet(Object e)
Initialize this to be a singleton set containing the given element.

See Also:
singleton(java.lang.Object)
Specifications: (class)pure
public normal_behavior
assignable objectState, elementType, containsNull, owner;
ensures this.has(e)&&this.int_size() == 1;
ensures_redundantly (* this is a singleton set containing e *);

JMLObjectSet

protected JMLObjectSet(nullable JMLListObjectNode ls,
                       int sz)
Initialize this set with the given instance variables.

Specifications: (class)pure
requires (ls == null) == (sz == 0);
requires sz >= 0;
assignable objectState, elementType, containsNull, owner;
ensures ls != null ==> this.elementType == ls.elementType;
ensures ls != null ==> this.containsNull == ls.containsNull;
ensures ls == null ==> this.elementType <: \type(java.lang.Object);
ensures ls == null ==> !this.containsNull;

JMLObjectSet

protected JMLObjectSet(nullable JMLListObjectNode ls)
Initialize this set with the given list.

Specifications: (class)pure
assignable objectState, elementType, containsNull, owner;
ensures ls != null ==> this.elementType == ls.elementType;
ensures ls != null ==> this.containsNull == ls.containsNull;
ensures ls == null ==> this.elementType <: \type(java.lang.Object);
ensures ls == null ==> !this.containsNull;
Model Method Detail

equational_theory

public static boolean equational_theory(JMLObjectSet s,
                                        JMLObjectSet s2,
                                        Object e1,
                                        Object e2)
An equational specification of the properties of sets.

Specifications: pure
public normal_behavior
{|
ensures \result <==> !(new org.jmlspecs.models.JMLObjectSet()).has(e1);
also
ensures \result <==> s.insert(null).has(e2) == (e2 == null||s.has(e2));
also
ensures \result <==> (e1 != null ==> s.insert(e1).has(e2) == (e1 == e2||s.has(e2)));
also
ensures \result <==> (new org.jmlspecs.models.JMLObjectSet()).int_size() == 0;
also
ensures \result <==> s.insert(e1).int_size() == (s.has(e1) ? s.int_size() : s.int_size()+1);
also
ensures \result <==> s.isSubset(s2) == ( \forall java.lang.Object o; ; s.has(o) ==> s2.has(o));
also
ensures \result <==> s.equals(s2) == (s.isSubset(s2)&&s2.isSubset(s));
also
ensures \result <==> (new org.jmlspecs.models.JMLObjectSet()).remove(e1).equals(new org.jmlspecs.models.JMLObjectSet());
also
ensures \result <==> s.insert(null).remove(e2).equals(e2 == null ? s : s.remove(e2).insert(null));
also
ensures \result <==> e1 != null ==> s.insert(e1).remove(e2).equals(e1 == e2 ? s : s.remove(e2).insert(e1));
also
ensures \result <==> (s.union(s2)).has(e1) == (s.has(e1)||s2.has(e1));
also
ensures \result <==> (s.intersection(s2)).has(e1) == (s.has(e1)&&s2.has(e1));
also
ensures \result <==> (s.difference(s2)).has(e1) == (s.has(e1)&&!s2.has(e1));
also
ensures \result <==> s.isEmpty() == (s.int_size() == 0);
also
ensures \result <==> (new org.jmlspecs.models.JMLObjectSet(e1)).equals(new org.jmlspecs.models.JMLObjectSet().insert(e1));
also
ensures \result <==> s.isProperSubset(s2) == (s.isSubset(s2)&&!s.equals(s2));
also
ensures \result <==> s.isSuperset(s2) == s2.isSubset(s);
also
ensures \result <==> s.isProperSuperset(s2) == s2.isProperSubset(s);
|}
    implies_that
ensures \result <==> (new org.jmlspecs.models.JMLObjectSet()).isEmpty();
ensures \result <==> !s.insert(e1).isEmpty();
ensures \result <==> (new org.jmlspecs.models.JMLObjectSet(null)).has(e2) == (e2 == null);
ensures \result <==> (e1 != null ==> new org.jmlspecs.models.JMLObjectSet(e1).has(e2) == (e1 == e2));
Method Detail

singleton

public static JMLObjectSet singleton(Object e)
Return the singleton set containing the given element.

See Also:
JMLObjectSet(Object)
Specifications: pure non_null
public normal_behavior
ensures \result != null&&\result .equals(new org.jmlspecs.models.JMLObjectSet(e));

convertFrom

public static JMLObjectSet convertFrom(non_null Object[] a)
Return the set containing all the elements in the given array.

Specifications: pure non_null
public normal_behavior
requires a != null;
ensures \result != null&&\result .int_size() == a.length&&( \forall int i; 0 <= i&&i < a.length; \result .has(a[i]));

convertFrom

public static JMLObjectSet convertFrom(non_null Collection c)
                                throws ClassCastException
Return the set containing all the object in the given collection.

Throws:
ClassCastException - if some element in c is not an instance of Object.
See Also:
containsAll(java.util.Collection)
Specifications: pure non_null
public normal_behavior
requires c != null&&( \forall java.lang.Object o; c.contains(o); o == null||(o instanceof java.lang.Object));
requires c.size() < 2147483647;
ensures \result != null&&\result .int_size() == c.size()&&( \forall java.lang.Object x; ; c.contains(x) <==> \result .has(x));
     also
public exceptional_behavior
requires c != null&&( \exists java.lang.Object o; c.contains(o); o != null&&!(o instanceof java.lang.Object));
signals_only java.lang.ClassCastException;

convertFrom

public static JMLObjectSet convertFrom(non_null JMLCollection c)
                                throws ClassCastException
Return the set containing all the object in the given JMLCollection.

Throws:
ClassCastException - if some element in c is not an instance of Object.
Specifications: pure non_null
public normal_behavior
requires c != null&&(c.elementType <: \type(java.lang.Object));
ensures \result != null&&( \forall java.lang.Object x; ; c.has(x) <==> \result .has(x));
     also
public exceptional_behavior
requires c != null&&( \exists java.lang.Object o; c.has(o); !(o instanceof java.lang.Object));
signals_only java.lang.ClassCastException;

has

public boolean has(Object elem)
Is the argument "==" to one of the objects in theSet.

Specified by:
has in interface JMLCollection
Specifications: pure
     also
public normal_behavior
requires elem != null;
ensures (* \result <==> elem is "==" to one of the objects in theSet *);
     also
public normal_behavior
requires elem == null;
ensures (* \result <==> null is one of the objects in theSet *);
     also
public normal_behavior
requires this.isEmpty();
ensures !\result ;
Specifications inherited from overridden method has(Object elem) in interface JMLCollection:
       pure
public normal_behavior
ensures (* \result <==> elem is equal to one of the elements in the collection. *);
ensures_redundantly !this.containsNull&&elem == null ==> !\result ;
ensures_redundantly elem != null&&!(\typeof(elem) <: this.elementType) ==> !\result ;

containsAll

public boolean containsAll(non_null Collection c)
Tell whether, for each element in the given collection, there is a "==" element in this set.

Parameters:
c - the collection whose elements are sought.
See Also:
isSuperset(JMLObjectSet), convertFrom(java.util.Collection)
Specifications: (class)pure
public normal_behavior
requires c != null;
ensures \result <==> ( \forall java.lang.Object o; c.contains(o); this.has(o));

equals

public boolean equals(nullable Object s2)
Description copied from interface: JMLType
Test whether this object's value is equal to the given argument.

Specified by:
equals in interface JMLType
Overrides:
equals in class Object
Specifications: (class)pure
     also
public normal_behavior
ensures \result <==> s2 != null&&s2 instanceof org.jmlspecs.models.JMLObjectSet&&( \forall java.lang.Object e; ; this.has(e) == ((org.jmlspecs.models.JMLObjectSet)s2).has(e));
ensures_redundantly \result ==> s2 != null&&s2 instanceof org.jmlspecs.models.JMLObjectSet&&this.containsNull == ((org.jmlspecs.models.JMLObjectSet)s2).containsNull;
Specifications inherited from overridden method equals(Object obj) in class Object:
       pure
public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);
     also
public normal_behavior
requires this == obj;
ensures \result ;
     also
public code normal_behavior
requires obj != null;
ensures \result <==> this == obj;
     also
diverges false;
ensures obj == null ==> !\result ;
Specifications inherited from overridden method equals(Object ob2) in interface JMLType:
       pure
     also
public normal_behavior
ensures \result ==> ob2 != null&&(* ob2 is not distinguishable from this, except by using mutation or == *);
    implies_that
public normal_behavior
{|
requires ob2 != null&&ob2 instanceof org.jmlspecs.models.JMLType;
ensures ((org.jmlspecs.models.JMLType)ob2).equals(this) == \result ;
also
requires ob2 == this;
ensures \result <==> true;
|}

hashCode

public int hashCode()
Return a hash code for this object.

Specified by:
hashCode in interface JMLType
Overrides:
hashCode in class Object
Specifications: (class)pure
Specifications inherited from overridden method in class Object:
public behavior
assignable objectState;
ensures (* \result is a hash code for this object *);
     also
public code normal_behavior
assignable \nothing;
Specifications inherited from overridden method in interface JMLType:
       pure

isEmpty

public boolean isEmpty()
Is the set empty.

See Also:
int_size(), has(Object)
Specifications: pure
public normal_behavior
ensures \result == ( \forall java.lang.Object e; ; !this.has(e));
     also
protected normal_behavior
ensures this.the_list == null <==> \result ;

int_size

public int int_size()
Tells the number of elements in the set.

Specified by:
int_size in interface JMLCollection
Specifications: pure
     also
public normal_behavior
ensures (this.isEmpty() ==> \result == 0)&&(!this.isEmpty() ==> ( \exists java.lang.Object e; this.has(e); \result == 1+(this.remove(e).int_size())));
    implies_that
ensures \result >= 0;
Specifications inherited from overridden method in interface JMLCollection:
       pure
public normal_behavior
requires this.size() <= 2147483647;
ensures \result == this.size();

isSubset

public boolean isSubset(non_null JMLObjectSet s2)
Tells whether this set is a subset of or equal to the argument.

See Also:
isProperSubset(JMLObjectSet), isSuperset(JMLObjectSet)
Specifications: (class)pure
public normal_behavior
requires s2 != null;
ensures \result <==> ( \forall java.lang.Object e; ; this.has(e) ==> s2.has(e));

isProperSubset

public boolean isProperSubset(non_null JMLObjectSet s2)
Tells whether this set is a subset of but not equal to the argument.

See Also:
isSubset(JMLObjectSet), isProperSuperset(JMLObjectSet)
Specifications: (class)pure
public normal_behavior
requires s2 != null;
ensures \result <==> this.isSubset(s2)&&!this.equals(s2);

isSuperset

public boolean isSuperset(non_null JMLObjectSet s2)
Tells whether this set is a superset of or equal to the argument.

See Also:
isProperSuperset(JMLObjectSet), isSubset(JMLObjectSet), containsAll(java.util.Collection)
Specifications: (class)pure
public normal_behavior
requires s2 != null;
ensures \result == s2.isSubset(this);

isProperSuperset

public boolean isProperSuperset(non_null JMLObjectSet s2)
Tells whether this set is a superset of but not equal to the argument.

See Also:
isSuperset(JMLObjectSet), isProperSubset(JMLObjectSet)
Specifications: (class)pure
public normal_behavior
requires s2 != null;
ensures \result == s2.isProperSubset(this);

choose

public Object choose()
              throws JMLNoSuchElementException
Return an arbitrary element of this.

Throws:
JMLNoSuchElementException - if this is empty.
See Also:
isEmpty(), elements()
Specifications: (class)pure
public normal_behavior
requires !this.isEmpty();
ensures ( \exists java.lang.Object e; this.has(e); (\result == null ==> e == null)&&(\result != null ==> \result == e));
     also
public exceptional_behavior
requires this.isEmpty();
signals_only org.jmlspecs.models.JMLNoSuchElementException;
    implies_that
protected behavior
ensures \result != null ==> \typeof(\result ) <: this.elementType;
ensures !this.containsNull ==> \result != null;
signals_only org.jmlspecs.models.JMLNoSuchElementException;
signals (org.jmlspecs.models.JMLNoSuchElementException) this.the_list == null;

clone

public Object clone()
Return a clone of this object. This method does not clone the elements of the set.

Specified by:
clone in interface JMLType
Overrides:
clone in class Object
Specifications: non_null (class)pure
     also
public normal_behavior
ensures \result != null&&\result instanceof org.jmlspecs.models.JMLObjectSet&&this.equals(\result );
Specifications inherited from overridden method in class Object:
       non_null
protected normal_behavior
requires this instanceof java.lang.Cloneable;
assignable \nothing;
ensures \result != null;
ensures \typeof(\result ) == \typeof(this);
ensures (* \result is a clone of this *);
     also
protected normal_behavior
requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);
     also
requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures java.lang.reflect.Array.getLength(\result ) == java.lang.reflect.Array.getLength(this);
ensures ( \forall int i; 0 <= i&&i < java.lang.reflect.Array.getLength(this); ( \exists java.lang.Object result_i; result_i == java.lang.reflect.Array.get(\result ,i); (result_i == null&&java.lang.reflect.Array.get(this,i) == null)||(result_i != null&&result_i.equals(java.lang.reflect.Array.get(this,i)))));
     also
protected exceptional_behavior
requires !(this instanceof java.lang.Cloneable);
assignable \nothing;
signals_only java.lang.CloneNotSupportedException;
     also
protected normal_behavior
requires \elemtype(\typeof(this)) <: \type(java.lang.Object);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(int);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((int[])\result ).length == ((int[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((int[])this).length; ((int[])\result )[i] == ((int[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(byte);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((byte[])\result ).length == ((byte[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((byte[])this).length; ((byte[])\result )[i] == ((byte[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(char);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((char[])\result ).length == ((char[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((char[])this).length; ((char[])\result )[i] == ((char[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(long);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((long[])\result ).length == ((long[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((long[])this).length; ((long[])\result )[i] == ((long[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(short);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((short[])\result ).length == ((short[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((short[])this).length; ((short[])\result )[i] == ((short[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(boolean);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((boolean[])\result ).length == ((boolean[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((boolean[])this).length; ((boolean[])\result )[i] == ((boolean[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(float);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((float[])\result ).length == ((float[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((float[])this).length; (java.lang.Float.isNaN(((float[])\result )[i])&&java.lang.Float.isNaN(((float[])this)[i]))||((float[])\result )[i] == ((float[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(double);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((double[])\result ).length == ((double[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((double[])this).length; (java.lang.Double.isNaN(((double[])\result )[i])&&java.lang.Double.isNaN(((double[])this)[i]))||((double[])\result )[i] == ((double[])this)[i]);
Specifications inherited from overridden method in interface JMLType:
       pure
     also
public normal_behavior
ensures \result != null;
ensures \result instanceof org.jmlspecs.models.JMLType;
ensures ((org.jmlspecs.models.JMLType)\result ).equals(this);
    implies_that
ensures \result != null&&\typeof(\result ) <: \type(org.jmlspecs.models.JMLType);

insert

public JMLObjectSet insert(Object elem)
                    throws IllegalStateException
Returns a new set that contains all the elements of this and also the given argument.

Throws:
IllegalStateException
See Also:
has(Object), remove(Object)
Specifications: non_null (class)pure
public normal_behavior
requires this.int_size() < 2147483647||this.has(elem);
ensures \result != null&&( \forall java.lang.Object e; ; \result .has(e) <==> this.has(e)||(e == null&&elem == null)||(e != null&&e == elem));
ensures_redundantly this.isSubset(\result )&&\result .has(elem)&&\result .int_size() == this.int_size()+(this.has(elem) ? 0 : 1);
     also
public normal_behavior
ensures elem == null ==> \result .containsNull;
ensures elem != null ==> \result .containsNull == this.containsNull;

fast_insert

protected JMLObjectSet fast_insert(Object elem)
Returns a new set that contains all the elements of this and also the given argument, assuming the argument is not in the set.

See Also:
insert(Object)
Specifications: non_null (class)pure
protected normal_behavior
requires !this.has(elem);
requires this.int_size() < 2147483647;
ensures \result != null&&( \forall java.lang.Object e; ; \result .has(e) <==> this.has(e)||(e == null&&elem == null)||(e != null&&e == elem));
ensures_redundantly this.isSubset(\result )&&\result .has(elem)&&\result .int_size() == this.int_size()+1;

remove

public JMLObjectSet remove(Object elem)
Returns a new set that contains all the elements of this except for the given argument.

See Also:
has(Object), insert(Object)
Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&( \forall java.lang.Object e; ; \result .has(e) <==> this.has(e)&&!((e == null&&elem == null)||(e != null&&e == elem)));
ensures_redundantly \result .isSubset(this)&&!\result .has(elem)&&\result .int_size() == this.int_size()-(this.has(elem) ? 1 : 0);
    implies_that
ensures \result != null&&(!this.containsNull ==> !\result .containsNull);

intersection

public JMLObjectSet intersection(non_null JMLObjectSet s2)
Returns a new set that contains all the elements that are in both this and the given argument.

See Also:
union(JMLObjectSet), difference(JMLObjectSet)
Specifications: non_null (class)pure
public normal_behavior
requires s2 != null;
ensures \result != null&&( \forall java.lang.Object e; ; \result .has(e) <==> this.has(e)&&s2.has(e));
    implies_that
ensures \result != null&&(!this.containsNull||!s2.containsNull ==> !\result .containsNull);

union

public JMLObjectSet union(non_null JMLObjectSet s2)
                   throws IllegalStateException
Returns a new set that contains all the elements that are in either this or the given argument.

Throws:
IllegalStateException
See Also:
intersection(JMLObjectSet), difference(JMLObjectSet)
Specifications: non_null (class)pure
public normal_behavior
requires s2 != null;
requires this.int_size() < 2147483647-s2.difference(this).int_size();
ensures \result != null&&( \forall java.lang.Object e; ; \result .has(e) <==> this.has(e)||s2.has(e));
    implies_that
ensures \result != null&&(!this.containsNull&&!s2.containsNull ==> !\result .containsNull);

difference

public JMLObjectSet difference(non_null JMLObjectSet s2)
Returns a new set that contains all the elements that are in this but not in the given argument.

See Also:
union(JMLObjectSet), difference(JMLObjectSet)
Specifications: non_null (class)pure
public normal_behavior
requires s2 != null;
ensures \result != null&&( \forall java.lang.Object e; ; \result .has(e) <==> this.has(e)&&!s2.has(e));
    implies_that
ensures \result != null&&(!this.containsNull ==> !\result .containsNull);

powerSet

public JMLObjectSet powerSet()
                      throws IllegalStateException
Returns a new set that is the set of all subsets of this. The implementation is by Tim Wahls.

Throws:
IllegalStateException
Specifications: non_null (class)pure
public normal_behavior
requires this.int_size() < 32;
ensures \result != null&&( \forall org.jmlspecs.models.JMLObjectSet s; ; s.isSubset(this) <==> \result .has(s));
ensures_redundantly \result != null&&(0 < this.size&&this.size <= 31 ==> \result .int_size() == (2 << (this.int_size()-1)));
    implies_that
ensures \result != null&&!\result .containsNull;
    for_example
public normal_example
requires this.isEmpty();
ensures \result != null&&\result .equals(new org.jmlspecs.models.JMLObjectSet(org.jmlspecs.models.JMLObjectSet.EMPTY));
ensures_redundantly \result .int_size() == 1;
       also
public normal_example
forall java.lang.Object a;
forall java.lang.Object b;
forall java.lang.Object c;
requires this.equals(new org.jmlspecs.models.JMLObjectSet(a).insert(b).insert(c))&&this.int_size() == 3;
ensures \result != null&&\result .int_size() == 8&&\result .has(org.jmlspecs.models.JMLObjectSet.EMPTY)&&\result .has(new org.jmlspecs.models.JMLObjectSet(a))&&\result .has(new org.jmlspecs.models.JMLObjectSet(b))&&\result .has(new org.jmlspecs.models.JMLObjectSet(c))&&\result .has(new org.jmlspecs.models.JMLObjectSet(a).insert(b))&&\result .has(new org.jmlspecs.models.JMLObjectSet(a).insert(c))&&\result .has(new org.jmlspecs.models.JMLObjectSet(b).insert(c))&&\result .has(new org.jmlspecs.models.JMLObjectSet(a).insert(b).insert(c));

toBag

public JMLObjectBag toBag()
Return a new JMLObjectBag containing all the elements of this.

See Also:
toSequence()
Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&( \forall java.lang.Object o; ; \result .count(o) == 1 <==> this.has(o));
    implies_that
ensures \result != null&&(this.containsNull <==> \result .containsNull);

toSequence

public JMLObjectSequence toSequence()
Return a new JMLObjectSequence containing all the elements of this.

See Also:
toBag(), toArray()
Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&( \forall java.lang.Object o; ; \result .count(o) == 1 <==> this.has(o));
    implies_that
ensures \result != null&&(this.containsNull <==> \result .containsNull);

toArray

public Object[] toArray()
Return a new array containing all the elements of this.

See Also:
toSequence()
Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&\result .length == this.int_size()&&( \forall java.lang.Object o; ; org.jmlspecs.models.JMLArrayOps.hasObjectIdentity(\result ,o) <==> this.has(o));
ensures_redundantly \result != null&&\result .length == this.int_size()&&( \forall int i; 0 <= i&&i < \result .length; org.jmlspecs.models.JMLArrayOps.hasObjectIdentity(\result ,\result [i]) == this.has(\result [i]));
    implies_that
ensures \result != null&&(this.containsNull <==> !\nonnullelements(\result ));

elements

public JMLObjectSetEnumerator elements()
Returns an Enumeration over this set.

See Also:
iterator()
Specifications: non_null (class)pure
public normal_behavior
ensures \fresh(\result )&&this.equals(\result .uniteratedElems);
    implies_that
ensures \result != null&&(this.containsNull == \result .returnsNull);

iterator

public JMLIterator iterator()
Returns an Iterator over this set.

Specified by:
iterator in interface JMLCollection
See Also:
elements()
Specifications: non_null (class)pure
     also
public normal_behavior
ensures \fresh(\result )&&\result .equals(new org.jmlspecs.models.JMLEnumerationToIterator(this.elements()));
Specifications inherited from overridden method in interface JMLCollection:
       pure non_null
public normal_behavior
ensures \fresh(\result )&&\result .elementType == this.elementType;
ensures !this.containsNull ==> !\result .returnsNull;

toString

public String toString()
Return a string representation of this object.

Overrides:
toString in class Object
Specifications: non_null (class)pure
     also
public normal_behavior
ensures (* \result is a string representation of this *);
Specifications inherited from overridden method in class Object:
       non_null
public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);
     also
public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);
     also
public code model_program { ... }
    implies_that
assignable objectState;
ensures \result != null;

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.