Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD

java.util
Class HashMap

java.lang.Object
  extended byjava.util.AbstractMap
      extended byjava.util.HashMap
All Implemented Interfaces:
Cloneable, Map, Serializable
Direct Known Subclasses:
CAugmentationMap.ContextMap, CGFCollectionMap.SetMap
public class HashMap
extends AbstractMap
implements Map, Cloneable, Serializable

JML's specification of java.util.HashMap.

Author:
Katie Becker, Gary T. Leavens

Class Specifications
public invariant this.initialCapacity >= 0;
public invariant this.loadFactor > 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));

Nested Class Summary
(package private) static class HashMap.Entry
           
 
Nested classes inherited from class java.util.AbstractMap
AbstractMap.SimpleEntry
 
Model Field Summary
 int initialCapacity
           
 
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.lang.Object
objectTimesFinalized, owner
 
Ghost fields inherited from interface java.util.Map
containsNull
 
Field Summary
(package private) static int DEFAULT_INITIAL_CAPACITY
           
(package private) static float DEFAULT_LOAD_FACTOR
           
[spec_public] (package private)  float loadFactor
           
(package private) static int MAXIMUM_CAPACITY
           
(package private)  int modCount
           
(package private) static Object NULL_KEY
           
(package private)  int size
           
(package private)  HashMap.Entry[] table
           
(package private)  int threshold
           
 
Fields inherited from class java.util.AbstractMap
keySet, values
 
Constructor Summary
HashMap()
           
HashMap(int initialCapacity)
           
HashMap(int initialCapacity, float loadFactor)
           
HashMap(Map m)
           
 
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
(package private)  void addEntry(int hash, Object key, Object value, int bucketIndex)
           
(package private)  int capacity()
           
 void clear()
           
 Object clone()
           
 boolean containsKey(nullable Object key)
           
 boolean containsValue(nullable Object value)
           
(package private)  void createEntry(int hash, Object key, Object value, int bucketIndex)
           
 Set entrySet()
           
(package private) static boolean eq(Object x, Object y)
           
 Object get(nullable Object key)
           
(package private)  HashMap.Entry getEntry(Object key)
           
(package private) static int hash(Object x)
           
(package private) static int indexFor(int h, int length)
           
(package private)  void init()
           
 boolean isEmpty()
           
 Set keySet()
           
(package private)  float loadFactor()
           
(package private) static Object maskNull(Object key)
           
(package private)  Iterator newEntryIterator()
           
(package private)  Iterator newKeyIterator()
           
(package private)  Iterator newValueIterator()
           
 Object put(nullable Object key, nullable Object value)
           
 void putAll(Map t)
           
(package private)  void putAllForCreate(Map m)
           
 Object remove(nullable Object key)
           
(package private)  HashMap.Entry removeEntryForKey(Object key)
           
(package private)  HashMap.Entry removeMapping(Object o)
           
(package private)  void resize(int newCapacity)
           
 int size()
           
(package private)  void transfer(HashMap.Entry[] newTable)
           
(package private) static Object unmaskNull(Object key)
           
 Collection values()
           
 
Methods inherited from class java.util.AbstractMap
equals, hashCode, toString
 
Methods inherited from class java.lang.Object
finalize, getClass, notify, notifyAll, wait, wait, wait
 
Methods inherited from interface java.util.Map
equals, hashCode
 

Model Field Detail

initialCapacity

public int initialCapacity
Field Detail

DEFAULT_INITIAL_CAPACITY

static final int DEFAULT_INITIAL_CAPACITY

MAXIMUM_CAPACITY

static final int MAXIMUM_CAPACITY

DEFAULT_LOAD_FACTOR

static final float DEFAULT_LOAD_FACTOR

table

transient HashMap.Entry[] table

size

transient int size

threshold

int threshold

loadFactor

final float loadFactor
Specifications: spec_public

modCount

transient volatile int modCount

NULL_KEY

static final Object NULL_KEY
Constructor Detail

HashMap

public HashMap(int initialCapacity,
               float loadFactor)
Specifications:
public normal_behavior
requires initialCapacity >= 0;
assignable theMap, this.initialCapacity, this.loadFactor;
ensures this.theMap != null&&this.theMap.isEmpty();
ensures this.initialCapacity == initialCapacity&&this.loadFactor == loadFactor;

HashMap

public HashMap(int initialCapacity)
Specifications:
public normal_behavior
assignable theMap, this.initialCapacity, this.loadFactor;
ensures this.theMap != null&&this.theMap.isEmpty();
ensures this.initialCapacity == initialCapacity&&this.loadFactor == 0.75;

HashMap

public HashMap()
Specifications:
public normal_behavior
assignable theMap, initialCapacity, loadFactor;
ensures this.theMap != null&&this.theMap.isEmpty();
ensures this.loadFactor == 0.75;
ensures this.initialCapacity == 16;

HashMap

public HashMap(Map m)
Specifications:
public normal_behavior
requires m != null;
assignable theMap, initialCapacity, loadFactor;
ensures this.loadFactor == 0.75&&this.theMap.equals(m.theMap);
Method Detail

init

void init()

maskNull

static Object maskNull(Object key)

unmaskNull

static Object unmaskNull(Object key)

hash

static int hash(Object x)

eq

static boolean eq(Object x,
                  Object y)

indexFor

static int indexFor(int h,
                    int length)

size

public int size()
Specified by:
size in interface Map
Overrides:
size in class AbstractMap
Specifications: (inherited)pure
Specifications inherited from overridden method in class AbstractMap:
      --- None ---
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
Overrides:
isEmpty in class AbstractMap
Specifications: (inherited)pure
Specifications inherited from overridden method in class AbstractMap:
      --- None ---
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);

get

public Object get(nullable Object key)
Specified by:
get in interface Map
Overrides:
get in class AbstractMap
Specifications: (inherited)pure
Specifications inherited from overridden method in class AbstractMap:
      --- None ---
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));

containsKey

public boolean containsKey(nullable Object key)
Specified by:
containsKey in interface Map
Overrides:
containsKey in class AbstractMap
Specifications: (inherited)pure
Specifications inherited from overridden method in class AbstractMap:
      --- None ---
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));

getEntry

HashMap.Entry getEntry(Object key)

put

public Object put(nullable Object key,
                  nullable Object value)
Specified by:
put in interface Map
Overrides:
put in class AbstractMap
Specifications inherited from overridden method in class AbstractMap:
      --- None ---
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 *);

putAllForCreate

void putAllForCreate(Map m)

resize

void resize(int newCapacity)

transfer

void transfer(HashMap.Entry[] newTable)

putAll

public void putAll(Map t)
Specified by:
putAll in interface Map
Overrides:
putAll in class AbstractMap
Specifications inherited from overridden method putAll(Map t) in class AbstractMap:
     also
requires t != null;
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;

remove

public Object remove(nullable Object key)
Specified by:
remove in interface Map
Overrides:
remove in class AbstractMap
Specifications inherited from overridden method in class AbstractMap:
      --- None ---
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)));

removeEntryForKey

HashMap.Entry removeEntryForKey(Object key)

removeMapping

HashMap.Entry removeMapping(Object o)

clear

public void clear()
Specified by:
clear in interface Map
Overrides:
clear in class AbstractMap
Specifications inherited from overridden method in class AbstractMap:
      --- None ---
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;

containsValue

public boolean containsValue(nullable Object value)
Specified by:
containsValue in interface Map
Overrides:
containsValue in class AbstractMap
Specifications: (inherited)pure
Specifications inherited from overridden method in class AbstractMap:
      --- None ---
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 *);

clone

public Object clone()
Overrides:
clone in class AbstractMap
Specifications:
     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 AbstractMap:
      --- None ---
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]);

addEntry

void addEntry(int hash,
              Object key,
              Object value,
              int bucketIndex)

createEntry

void createEntry(int hash,
                 Object key,
                 Object value,
                 int bucketIndex)

newKeyIterator

Iterator newKeyIterator()

newValueIterator

Iterator newValueIterator()

newEntryIterator

Iterator newEntryIterator()

keySet

public Set keySet()
Specified by:
keySet in interface Map
Overrides:
keySet in class AbstractMap
Specifications: (inherited)pure
Specifications inherited from overridden method in class AbstractMap:
      --- None ---
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));

values

public Collection values()
Specified by:
values in interface Map
Overrides:
values in class AbstractMap
Specifications: (inherited)pure
Specifications inherited from overridden method in class AbstractMap:
      --- None ---
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));

entrySet

public Set entrySet()
Specified by:
entrySet in interface Map
Specifications: (inherited)pure
Specifications inherited from overridden method in class AbstractMap:
      --- None ---
Specifications inherited from overridden method in interface Map:
       pure
public normal_behavior
ensures \result != null;
ensures \result .theSet.equals(this.theMap);

capacity

int capacity()

loadFactor

float loadFactor()
Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD
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.