org.jmlspecs.models
Class JMLValueSet

java.lang.Object
  org.jmlspecs.models.JMLValueSetSpecs
      org.jmlspecs.models.JMLValueSet

All Implemented Interfaces:

Cloneable, JMLCollection, JMLType, JMLValueType, Serializable

public class JMLValueSet

extends JMLValueSetSpecs

implements JMLCollection

Sets of values. This type uses ".equals" to compare elements, and clones 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;

Version:

$Revision: 1.84 $

Author:

Gary T. Leavens, with help from Albert Baker, Clyde Ruby, and others.

See Also:

JMLCollection, JMLType, JMLEqualsSet, JMLObjectSet, JMLValueSetEnumerator, JMLValueSetSpecs, JMLObjectBag, JMLEqualsBag, JMLValueBag

Class Specifications

public invariant ( \forall org.jmlspecs.models.JMLValueSet s2; s2 != null; ( \forall org.jmlspecs.models.JMLType e1, e2; ; equational_theory(this,s2,e1,e2))); public invariant this.elementType <: \type(org.jmlspecs.models.JMLType); public invariant ( \forall org.jmlspecs.models.JMLType 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 JMLValueSet	EMPTY           The empty JMLValueSet.
[spec_public] protected  int	size           The number of elements in this set.
protected  JMLListValueNode	the_list           The list representing the elements of this set.

 

Constructor Summary
	JMLValueSet()           Initialize this to be an empty set.
protected	JMLValueSet(nullable JMLListValueNode ls)           Initialize this set with the given list.
protected	JMLValueSet(nullable JMLListValueNode ls, int sz)           Initialize this set with the given instance variables.
	JMLValueSet(JMLType e)           Initialize this to be a singleton set containing the given element.

 

Model Method Summary
static boolean	equational_theory(JMLValueSet s, JMLValueSet s2, JMLType e1, JMLType e2)           An equational specification of the properties of sets.

 

Model methods inherited from class org.jmlspecs.models.JMLValueSetSpecs

hasObject

 

Model methods inherited from class java.lang.Object

hashValue

 

Model methods inherited from interface org.jmlspecs.models.JMLCollection

size

 

Method Summary
JMLType	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 ".equals" element in this set.
static JMLValueSet	convertFrom(non_null Collection c)           Return the set containing all the value in the given collection.
static JMLValueSet	convertFrom(non_null JMLCollection c)           Return the set containing all the value in the given JMLCollection.
static JMLValueSet	convertFrom(non_null JMLType[] a)           Return the set containing all the elements in the given array.
JMLValueSet	difference(non_null JMLValueSet s2)           Returns a new set that contains all the elements that are in this but not in the given argument.
JMLValueSetEnumerator	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  JMLValueSet	fast_insert(JMLType 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(JMLType elem)           Is the argument ".equals" to one of the values in theSet.
int	hashCode()           Return a hash code for this object.
JMLValueSet	insert(JMLType 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.
JMLValueSet	intersection(non_null JMLValueSet 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 JMLValueSet s2)           Tells whether this set is a subset of but not equal to the argument.
boolean	isProperSuperset(non_null JMLValueSet s2)           Tells whether this set is a superset of but not equal to the argument.
boolean	isSubset(non_null JMLValueSet s2)           Tells whether this set is a subset of or equal to the argument.
boolean	isSuperset(non_null JMLValueSet s2)           Tells whether this set is a superset of or equal to the argument.
JMLIterator	iterator()           Returns an Iterator over this set.
JMLValueSet	powerSet()           Returns a new set that is the set of all subsets of this.
JMLValueSet	remove(JMLType elem)           Returns a new set that contains all the elements of this except for the given argument.
static JMLValueSet	singleton(JMLType e)           Return the singleton set containing the given element.
JMLType[]	toArray()           Return a new array containing all the elements of this.
JMLValueBag	toBag()           Return a new JMLValueBag containing all the elements of this.
JMLValueSequence	toSequence()           Return a new JMLValueSequence containing all the elements of this.
String	toString()           Return a string representation of this object.
JMLValueSet	union(non_null JMLValueSet s2)           Returns a new set that contains all the elements that are in either this or the given argument.

 

Methods inherited from class org.jmlspecs.models.JMLValueSetSpecs

has

 

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

 

Methods inherited from interface org.jmlspecs.models.JMLCollection

has

 

Field Detail

the_list

protected final JMLListValueNode 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 JMLValueSet EMPTY

The empty JMLValueSet.

See Also:

JMLValueSet()

Specifications: non_null

JMLValueSet

public JMLValueSet()

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(org.jmlspecs.models.JMLType)&&!this.containsNull;

JMLValueSet

public JMLValueSet(JMLType e)

Initialize this to be a singleton set containing the given element.

See Also:

singleton(org.jmlspecs.models.JMLType)

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 *);

     also

public model_program { ... }

JMLValueSet

protected JMLValueSet(nullable JMLListValueNode 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(org.jmlspecs.models.JMLType);
ensures ls == null ==> !this.containsNull;

JMLValueSet

protected JMLValueSet(nullable JMLListValueNode 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(org.jmlspecs.models.JMLType);
ensures ls == null ==> !this.containsNull;

equational_theory

public static boolean equational_theory(JMLValueSet s,
                                        JMLValueSet s2,
                                        JMLType e1,
                                        JMLType e2)

An equational specification of the properties of sets.

Specifications: pure

public normal_behavior

{|

ensures \result <==> !(new org.jmlspecs.models.JMLValueSet()).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.equals(e2)||s.has(e2)));

also

ensures \result <==> (new org.jmlspecs.models.JMLValueSet()).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 org.jmlspecs.models.JMLType 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.JMLValueSet()).remove(e1).equals(new org.jmlspecs.models.JMLValueSet());

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.equals(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.JMLValueSet(e1)).equals(new org.jmlspecs.models.JMLValueSet().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.JMLValueSet()).isEmpty();
ensures \result <==> !s.insert(e1).isEmpty();
ensures \result <==> (new org.jmlspecs.models.JMLValueSet(null)).has(e2) == (e2 == null);
ensures \result <==> (e1 != null ==> new org.jmlspecs.models.JMLValueSet(e1).has(e2) == (e1.equals(e2)));

singleton

public static JMLValueSet singleton(JMLType e)

Return the singleton set containing the given element.

See Also:

JMLValueSet(JMLType)

Specifications: pure non_null

public normal_behavior
ensures \result != null&&\result .equals(new org.jmlspecs.models.JMLValueSet(e));

convertFrom

public static JMLValueSet convertFrom(non_null JMLType[] 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 JMLValueSet convertFrom(non_null Collection c)
                               throws ClassCastException

Return the set containing all the value in the given collection.

Throws:

ClassCastException - if some element in c is not an instance of JMLType.

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 org.jmlspecs.models.JMLType));
requires c.size() < 2147483647;
ensures \result != null&&\result .int_size() == c.size()&&( \forall org.jmlspecs.models.JMLType 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 org.jmlspecs.models.JMLType));
signals_only java.lang.ClassCastException;

convertFrom

public static JMLValueSet convertFrom(non_null JMLCollection c)
                               throws ClassCastException

Return the set containing all the value in the given JMLCollection.

Throws:

ClassCastException - if some element in c is not an instance of JMLType.

Specifications: pure non_null

public normal_behavior
requires c != null&&(c.elementType <: \type(org.jmlspecs.models.JMLType));
ensures \result != null&&( \forall org.jmlspecs.models.JMLType x; ; c.has(x) <==> \result .has(x));

     also

public exceptional_behavior
requires c != null&&( \exists java.lang.Object o; c.has(o); !(o instanceof org.jmlspecs.models.JMLType));
signals_only java.lang.ClassCastException;

has

public boolean has(JMLType elem)

Is the argument ".equals" to one of the values in theSet.

Specifications: pure

     also

public normal_behavior
requires elem != null;
ensures (* \result <==> elem is ".equals" to one of the values in theSet *);

     also

public normal_behavior
requires elem == null;
ensures (* \result <==> null is one of the values in theSet *);

     also

public normal_behavior
requires this.isEmpty();
ensures !\result ;

Specifications inherited from overridden method has(JMLType elem) in class JMLValueSetSpecs:
       (class)pure

public normal_behavior
ensures \result <==> (* elem tests as ".equals" to one of the objects in the set *);

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 ".equals" element in this set.

Parameters:

c - the collection whose elements are sought.

See Also:

isSuperset(JMLValueSet), 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.JMLValueSet&&( \forall org.jmlspecs.models.JMLType e; ; this.has(e) == ((org.jmlspecs.models.JMLValueSet)s2).has(e));
ensures_redundantly \result ==> s2 != null&&s2 instanceof org.jmlspecs.models.JMLValueSet&&this.containsNull == ((org.jmlspecs.models.JMLValueSet)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;

|}

Specifications inherited from overridden method equals(Object ob2) in interface JMLValueType:
       pure

     also

public normal_behavior
ensures \result ==> ob2 != null&&(* all externally-visible objects contained in ob2 test as ".equals()" to the corresponding object in this (and vice versa) *);

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(JMLType)

Specifications: pure

public normal_behavior
ensures \result == ( \forall org.jmlspecs.models.JMLType 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 org.jmlspecs.models.JMLType e; this.has(e); \result == 1+(this.remove(e).int_size())));

    implies_that

ensures \result >= 0;

Specifications inherited from overridden method in class JMLValueSetSpecs:
       (class)pure

public normal_behavior
ensures \result >= 0&&(* \result is the number of elements in the set *);

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 JMLValueSet s2)

Tells whether this set is a subset of or equal to the argument.

See Also:

isProperSubset(JMLValueSet), isSuperset(JMLValueSet)

Specifications: (class)pure

public normal_behavior
requires s2 != null;
ensures \result <==> ( \forall org.jmlspecs.models.JMLType e; ; this.has(e) ==> s2.has(e));

isProperSubset

public boolean isProperSubset(non_null JMLValueSet s2)

Tells whether this set is a subset of but not equal to the argument.

See Also:

isSubset(JMLValueSet), isProperSuperset(JMLValueSet)

Specifications: (class)pure

public normal_behavior
requires s2 != null;
ensures \result <==> this.isSubset(s2)&&!this.equals(s2);

isSuperset

public boolean isSuperset(non_null JMLValueSet s2)

Tells whether this set is a superset of or equal to the argument.

See Also:

isProperSuperset(JMLValueSet), isSubset(JMLValueSet), containsAll(java.util.Collection)

Specifications: (class)pure

public normal_behavior
requires s2 != null;
ensures \result == s2.isSubset(this);

isProperSuperset

public boolean isProperSuperset(non_null JMLValueSet s2)

Tells whether this set is a superset of but not equal to the argument.

See Also:

isSuperset(JMLValueSet), isProperSubset(JMLValueSet)

Specifications: (class)pure

public normal_behavior
requires s2 != null;
ensures \result == s2.isProperSubset(this);

choose

public JMLType 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 org.jmlspecs.models.JMLType e; this.has(e); (\result == null ==> e == null)&&(\result != null ==> \result .equals(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 clones the elements of the set.

Specified by:

clone in interface JMLType

Specified by:

clone in class JMLValueSetSpecs

Specifications: non_null (class)pure

     also

public normal_behavior
ensures \result != null&&\result instanceof org.jmlspecs.models.JMLValueSet&&this.equals(\result );

Specifications inherited from overridden method in class JMLValueSetSpecs:
       (class)pure

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

Specifications inherited from overridden method in interface JMLValueType:
       pure

     also

public normal_behavior
ensures \result instanceof org.jmlspecs.models.JMLValueType&&(* all externally-visible mutable objects contained directly in "this" must be cloned in \result. *);

    implies_that

ensures (* no direct aliases are created between this and \result *);

insert

public JMLValueSet insert(JMLType elem)
                   throws IllegalStateException

Returns a new set that contains all the elements of this and also the given argument.

Throws:

IllegalStateException

See Also:

has(JMLType), remove(JMLType)

Specifications: non_null (class)pure

     also

public normal_behavior
requires this.int_size() < 2147483647||this.has(elem);
ensures \result != null&&( \forall org.jmlspecs.models.JMLType e; ; \result .has(e) <==> this.has(e)||(e == null&&elem == null)||(e != null&&e.equals(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;

Specifications inherited from overridden method in class JMLValueSetSpecs:
       non_null (class)pure

fast_insert

protected JMLValueSet fast_insert(JMLType 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(JMLType)

Specifications: non_null (class)pure

protected normal_behavior
requires !this.has(elem);
requires this.int_size() < 2147483647;
ensures \result != null&&( \forall org.jmlspecs.models.JMLType e; ; \result .has(e) <==> this.has(e)||(e == null&&elem == null)||(e != null&&e.equals(elem)));
ensures_redundantly this.isSubset(\result )&&\result .has(elem)&&\result .int_size() == this.int_size()+1;

remove

public JMLValueSet remove(JMLType elem)

Returns a new set that contains all the elements of this except for the given argument.

See Also:

has(JMLType), insert(JMLType)

Specifications: non_null (class)pure

public normal_behavior
ensures \result != null&&( \forall org.jmlspecs.models.JMLType e; ; \result .has(e) <==> this.has(e)&&!((e == null&&elem == null)||(e != null&&e.equals(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 JMLValueSet intersection(non_null JMLValueSet s2)

Returns a new set that contains all the elements that are in both this and the given argument.

See Also:

union(JMLValueSet), difference(JMLValueSet)

Specifications: non_null (class)pure

public normal_behavior
requires s2 != null;
ensures \result != null&&( \forall org.jmlspecs.models.JMLType e; ; \result .has(e) <==> this.has(e)&&s2.has(e));

    implies_that

ensures \result != null&&(!this.containsNull||!s2.containsNull ==> !\result .containsNull);

union

public JMLValueSet union(non_null JMLValueSet 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(JMLValueSet), difference(JMLValueSet)

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 org.jmlspecs.models.JMLType e; ; \result .has(e) <==> this.has(e)||s2.has(e));

    implies_that

ensures \result != null&&(!this.containsNull&&!s2.containsNull ==> !\result .containsNull);

difference

public JMLValueSet difference(non_null JMLValueSet s2)

Returns a new set that contains all the elements that are in this but not in the given argument.

See Also:

union(JMLValueSet), difference(JMLValueSet)

Specifications: non_null (class)pure

public normal_behavior
requires s2 != null;
ensures \result != null&&( \forall org.jmlspecs.models.JMLType e; ; \result .has(e) <==> this.has(e)&&!s2.has(e));

    implies_that

ensures \result != null&&(!this.containsNull ==> !\result .containsNull);

powerSet

public JMLValueSet 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.JMLValueSet 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.JMLValueSet(org.jmlspecs.models.JMLValueSet.EMPTY));
ensures_redundantly \result .int_size() == 1;

       also

public normal_example
forall org.jmlspecs.models.JMLType a;
forall org.jmlspecs.models.JMLType b;
forall org.jmlspecs.models.JMLType c;
requires this.equals(new org.jmlspecs.models.JMLValueSet(a).insert(b).insert(c))&&this.int_size() == 3;
ensures \result != null&&\result .int_size() == 8&&\result .has(org.jmlspecs.models.JMLValueSet.EMPTY)&&\result .has(new org.jmlspecs.models.JMLValueSet(a))&&\result .has(new org.jmlspecs.models.JMLValueSet(b))&&\result .has(new org.jmlspecs.models.JMLValueSet(c))&&\result .has(new org.jmlspecs.models.JMLValueSet(a).insert(b))&&\result .has(new org.jmlspecs.models.JMLValueSet(a).insert(c))&&\result .has(new org.jmlspecs.models.JMLValueSet(b).insert(c))&&\result .has(new org.jmlspecs.models.JMLValueSet(a).insert(b).insert(c));

toBag

public JMLValueBag toBag()

Return a new JMLValueBag containing all the elements of this.

See Also:

toSequence()

Specifications: non_null (class)pure

public normal_behavior
ensures \result != null&&( \forall org.jmlspecs.models.JMLType o; ; \result .count(o) == 1 <==> this.has(o));

    implies_that

ensures \result != null&&(this.containsNull <==> \result .containsNull);

toSequence

public JMLValueSequence toSequence()

Return a new JMLValueSequence containing all the elements of this.

See Also:

toBag(), toArray()

Specifications: non_null (class)pure

public normal_behavior
ensures \result != null&&( \forall org.jmlspecs.models.JMLType o; ; \result .count(o) == 1 <==> this.has(o));

    implies_that

ensures \result != null&&(this.containsNull <==> \result .containsNull);

toArray

public JMLType[] 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 org.jmlspecs.models.JMLType o; ; org.jmlspecs.models.JMLArrayOps.hasValueEquals(\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.hasValueEquals(\result ,\result [i]) == this.has(\result [i]));

    implies_that

ensures \result != null&&(this.containsNull <==> !\nonnullelements(\result ));

elements

public JMLValueSetEnumerator 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;