java.util
Class Hashtable

java.lang.Object
  java.util.Dictionary
      java.util.Hashtable

All Implemented Interfaces:

Cloneable, Map, Serializable

Direct Known Subclasses:

Properties

public class Hashtable

extends Dictionary

implements Map, Cloneable, Serializable

JML's specification of java.util.Hashtable.

Version:

$Revision: 1.14 $

Author:

Katie Becker, Gary T. Leavens

Class Specifications

public invariant this.initialCapacity >= 0; public invariant this.mLoadFactor > 0.0;

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Specifications inherited from interface Map

axiom ( \forall java.util.Map m; ; ( \forall java.lang.Object k, v, vv; ; (m.contains(k,v)&&m.contains(k,vv)) ==> nullequals(v,vv))); instance public invariant ( \forall java.lang.Object o; this.theMap.has(o); o instanceof java.util.Map.Entry); instance public invariant ( \forall java.lang.Object o1, o2; this.theMap.has(o1)&&this.theMap.has(o2); o2 != o1 ==> !org.jmlspecs.models.JMLNullSafe.equals(o2,o1));

Model Field Summary
int	initialCapacity
float	mLoadFactor

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Model fields inherited from interface java.util.Map

theMap

 

Ghost Field Summary

 

Ghost fields inherited from class java.util.Dictionary

elementType, keyType

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Ghost fields inherited from interface java.util.Map

containsNull

 

Constructor Summary

Hashtable()

Hashtable(int initialCapacity)

Hashtable(int initialCapacity, float mLoadFactor)

Hashtable(Map t)

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Model methods inherited from interface java.util.Map

contains, contains, nullequals

 

Method Summary
void	clear()
Object	clone()
boolean	contains(Object value)
boolean	containsKey(nullable Object key)
boolean	containsValue(nullable Object value)
Enumeration	elements()
Set	entrySet()
boolean	equals(nullable Object o)
Object	get(nullable Object key)
int	hashCode()
boolean	isEmpty()
Enumeration	keys()
Set	keySet()
Object	put(nullable Object key, nullable Object value)
void	putAll(Map t)
protected  void	rehash()
Object	remove(nullable Object key)
int	size()
String	toString()
Collection	values()

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

initialCapacity

public int initialCapacity

mLoadFactor

public float mLoadFactor

Hashtable

public Hashtable(int initialCapacity,
                 float mLoadFactor)

Specifications:

public normal_behavior
requires initialCapacity >= 0;
assignable theMap, this.initialCapacity, this.mLoadFactor;
ensures this.theMap != null&&this.theMap.isEmpty();
ensures this.initialCapacity == initialCapacity&&this.mLoadFactor == mLoadFactor;

Hashtable

public Hashtable(int initialCapacity)

Specifications:

public normal_behavior
assignable theMap, this.initialCapacity, this.mLoadFactor;
ensures this.theMap != null&&this.theMap.isEmpty();
ensures this.initialCapacity == initialCapacity&&this.mLoadFactor == 0.75;

Hashtable

public Hashtable()

Specifications:

public normal_behavior
assignable theMap, initialCapacity, mLoadFactor;
ensures this.theMap != null&&this.theMap.isEmpty();
ensures this.mLoadFactor == 0.75;

Hashtable

public Hashtable(Map t)

Specifications:

public normal_behavior
requires t != null;
assignable theMap, initialCapacity, mLoadFactor;
ensures this.initialCapacity == 2*(t.theMap.int_size());
ensures this.mLoadFactor == 0.75&&this.theMap.equals(t.theMap);

size

public int size()

Specified by:

size in interface Map

Specifications: (inherited)pure

Specifications inherited from overridden method in class Dictionary:

assignable \nothing;

Specifications inherited from overridden method in interface Map:
       pure

public normal_behavior
ensures \result == this.theMap.int_size();

    implies_that

ensures \result >= 0;

isEmpty

public boolean isEmpty()

Specified by:

isEmpty in interface Map

Specifications: (inherited)pure

Specifications inherited from overridden method in class Dictionary:

assignable \nothing;

Specifications inherited from overridden method in interface Map:
       pure

public normal_behavior
ensures \result <==> this.theMap.isEmpty();

    implies_that

public normal_behavior
ensures \result <==> (this.size() == 0);

keys

public Enumeration keys()

Specifications: pure

     also

normal_behavior
ensures \fresh(\result );

Specifications inherited from overridden method in class Dictionary:
       non_null

assignable \nothing;

elements

public Enumeration elements()

Specifications: pure

     also

normal_behavior
ensures \fresh(\result );

Specifications inherited from overridden method in class Dictionary:
       non_null

assignable \nothing;

contains

public boolean contains(Object value)

Specifications: pure

public normal_behavior
requires value != null;
ensures \result <==> ( \exists java.util.Map.Entry e; this.theMap.has(e)&&e != null; e.abstractValue.equals(value));
ensures_redundantly \result == this.containsValue(value);

containsValue

public boolean containsValue(nullable Object value)

Specified by:

containsValue in interface Map

Specifications: (inherited)pure

     also

public behavior
ensures value != null;
signals_only java.lang.NullPointerException;
signals (java.lang.NullPointerException) value == null;

Specifications inherited from overridden method containsValue(Object value) in interface Map:
       pure

public behavior
ensures \result <==> ( \exists java.util.Map.Entry e; this.theMap.has(e)&&e != null; org.jmlspecs.models.JMLNullSafe.equals(e.abstractValue,value));
signals_only java.lang.ClassCastException, java.lang.NullPointerException;
signals (java.lang.ClassCastException) (* if the value is not appropriate for this object *);
signals (java.lang.NullPointerException) value == null&&(* this type doesn't permit null values *);

containsKey

public boolean containsKey(nullable Object key)

Specified by:

containsKey in interface Map

Specifications: (inherited)pure

Specifications inherited from overridden method containsKey(Object key) in interface Map:
       pure

public normal_behavior
ensures \result <==> ( \exists java.util.Map.Entry e; this.theMap.has(e)&&e != null; org.jmlspecs.models.JMLNullSafe.equals(e.abstractKey,key));

get

public Object get(nullable Object key)

Specified by:

get in interface Map

Specifications: (inherited)pure

Specifications inherited from overridden method get(Object key) in class Dictionary:
       nullable

requires key != null;
assignable \nothing;

Specifications inherited from overridden method get(Object key) in interface Map:
       pure nullable

public normal_behavior
requires !this.containsKey(key);
ensures \result == null;

     also

public normal_behavior
requires this.containsKey(key);
ensures ( \exists java.util.Map.Entry e; this.theMap.has(e); e != null&&org.jmlspecs.models.JMLNullSafe.equals(e.abstractKey,key)&&\result .equals(e.abstractValue));

rehash

protected void rehash()

Specifications:

protected normal_behavior
assignable theMap;
ensures this.theMap.equals(\old(this.theMap));

put

public Object put(nullable Object key,
                  nullable Object value)

Specified by:

put in interface Map

Specifications inherited from overridden method put(Object key, Object value) in class Dictionary:
       nullable

requires key != null;
requires value != null;

Specifications inherited from overridden method put(Object key, Object value) in interface Map:

public behavior
assignable objectState;
ensures ( \exists java.util.Map.Entry e; this.theMap.has(e); e != null&&org.jmlspecs.models.JMLNullSafe.equals(e.abstractKey,key)&&org.jmlspecs.models.JMLNullSafe.equals(e.abstractValue,value));

     also

public behavior
assignable objectState;
ensures ( \exists java.util.Map.Entry e; this.contains(e); nullequals(e.abstractKey,key)&&nullequals(e.abstractValue,value));
ensures ( \forall java.util.Map.Entry e; ; \old(this.contains(e)) ==> this.contains(e));
ensures ( \forall java.util.Map.Entry e; ; this.contains(e) ==> (\old(this.contains(e))||(e.getKey() == key&&e.getValue() == value)));
ensures \result == \old(this.get(key));
signals_only java.lang.RuntimeException;
signals (java.lang.NullPointerException) \not_modified(value)&&(key == null)||(value == null)&&!this.containsNull;
signals (java.lang.UnsupportedOperationException) \not_modified(theMap)&&(* if the map's put operation is not supported *);
signals (java.lang.ClassCastException) \not_modified(theMap)&&(* \typeof(key) or \typeof(value) is incompatible with the valueType or keyType of this map *);
signals (java.lang.IllegalArgumentException) \not_modified(theMap)&&(* if some aspect of key or value is not allowed in the map *);

remove

public Object remove(nullable Object key)

Specified by:

remove in interface Map

Specifications inherited from overridden method remove(Object key) in class Dictionary:
       nullable

requires key != null;

Specifications inherited from overridden method remove(Object key) in interface Map:

public behavior
assignable theMap;
ensures \result != null ==> ( \exists java.util.Map.Entry e; e != null&&\old(this.theMap.has(e)); org.jmlspecs.models.JMLNullSafe.equals(e.abstractKey,key)&&\result .equals(e.abstractValue));
ensures !( \exists java.util.Map.Entry e; e != null&&\old(this.theMap.has(e)); org.jmlspecs.models.JMLNullSafe.equals(e.abstractKey,key));
signals_only java.lang.RuntimeException;

     also

public behavior
assignable objectState;
ensures ( \forall java.util.Map.Entry e; ; this.contains(e) ==> \old(this.contains(e)));
ensures ( \forall java.util.Map.Entry e; \old(this.contains(e)); (this.contains(e)||nullequals(key,e.getKey())));
ensures \old(this.containsKey(key)) ==> nullequals(\result ,\old(this.get(key)));
ensures !\old(this.containsKey(key)) ==> \result == null;
signals_only java.lang.RuntimeException;
signals (java.lang.UnsupportedOperationException) (* if this operation is not supported *);
signals (java.lang.ClassCastException) (* if the argument is not appropriate *);
signals (java.lang.NullPointerException) key == null&&(* if this map doesn't support null keys *);

    implies_that

assignable objectState;
ensures !this.containsKey(key);
ensures ( \forall java.util.Map.Entry e; ; this.theMap.has(e) ==> \old(this.theMap.has(e)));
ensures ( \forall java.util.Map.Entry e; \old(this.theMap.has(e)); (this.theMap.has(e)||org.jmlspecs.models.JMLNullSafe.equals(e.abstractKey,key)));

putAll

public void putAll(Map t)

Specified by:

putAll in interface Map

Specifications inherited from overridden method putAll(Map t) in interface Map:

public behavior
assignable theMap;
ensures ( \forall java.util.Map.Entry e; t.theMap.has(e); this.theMap.has(e));
signals_only java.lang.RuntimeException;
signals (java.lang.NullPointerException) \not_modified(theMap)&&(t == null)&&!this.containsNull;
signals (java.lang.UnsupportedOperationException) \not_modified(theMap)&&(* if the map's put operation is not supported *);
signals (java.lang.ClassCastException) \not_modified(theMap)&&(* \typeof(t) or is incompatible with this map *);
signals (java.lang.IllegalArgumentException) \not_modified(theMap)&&(* if some aspect of a key or value is not allowed in the map *);

     also

public behavior
assignable objectState;
ensures ( \forall java.util.Map.Entry e; ; \old(this.contains(e)) ==> this.contains(e));
ensures ( \forall java.util.Map.Entry e; ; \old(t.contains(e)) ==> this.contains(e));
ensures ( \forall java.util.Map.Entry e; ; this.contains(e) ==> (\old(this.contains(e))||\old(t.contains(e))));
signals_only java.lang.RuntimeException;

clear

public void clear()

Specified by:

clear in interface Map

Specifications inherited from overridden method in interface Map:

public behavior
assignable theMap;
ensures this.theMap.isEmpty();
signals_only java.lang.RuntimeException;

    implies_that

public behavior
assignable objectState;
ensures this.isEmpty();
signals_only java.lang.RuntimeException;

clone

public Object clone()

Overrides:

clone in class Object

Specifications: pure

     also

public normal_behavior
assignable \nothing;
ensures \result instanceof java.util.Map&&\fresh(\result )&&((java.util.Map)\result ).equals(this);
ensures_redundantly \result != this;

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

toString

public String toString()

Overrides:

toString in class Object

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;

keySet

public Set keySet()

Specified by:

keySet in interface Map

Specifications: (inherited)pure

Specifications inherited from overridden method in interface Map:
       pure

public normal_behavior
ensures_redundantly \result != null;
ensures ( \forall java.lang.Object o; ; this.containsKey(o) <==> \result .contains(o));

entrySet

public Set entrySet()

Specified by:

entrySet in interface Map

Specifications: (inherited)pure

Specifications inherited from overridden method in interface Map:
       pure

public normal_behavior
ensures \result != null;
ensures \result .theSet.equals(this.theMap);

values

public Collection values()

Specified by:

values in interface Map

Specifications: (inherited)pure

Specifications inherited from overridden method in interface Map:
       pure

public normal_behavior
ensures \result != null;
ensures ( \forall java.lang.Object o; ; \result .contains(o) <==> this.containsValue(o));

equals

public boolean equals(nullable Object o)

Specified by:

equals in interface Map

Overrides:

equals in class Object

Specifications: (inherited)pure

     also

public normal_behavior
requires o instanceof java.util.Hashtable;
ensures \result <==> this.theMap.equals(((java.util.Hashtable)o).theMap);

     also

public normal_behavior
requires !(o instanceof java.util.Hashtable);
ensures \result == false;

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 o) in interface Map:
       pure

     also

public normal_behavior
requires o instanceof java.util.Map;
ensures \result ==> this.theMap.equals(o);

     also

public normal_behavior
requires o instanceof java.util.Map;
ensures \result ==> ( \forall java.util.Map.Entry e; ; this.contains(e) <==> ((java.util.Map)o).contains(e));

     also

public normal_behavior
requires !(o instanceof java.util.Map);
ensures \result == false;

hashCode

public int hashCode()

Specified by:

hashCode in interface Map

Overrides:

hashCode in class Object

Specifications: (inherited)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 Map:
       pure