java.util
Class AbstractMap

java.lang.Object
  java.util.AbstractMap

All Implemented Interfaces:

Map

Direct Known Subclasses:

HashMap, TreeMap

public abstract class AbstractMap

extends Object

implements Map

Class Specifications

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	AbstractMap.SimpleEntry

 

Model Field Summary

 

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)  Set	keySet
(package private)  Collection	values

 

Constructor Summary
protected	AbstractMap()

 

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()
protected  Object	clone()
boolean	containsKey(nullable Object key)
boolean	containsValue(nullable Object value)
abstract  Set	entrySet()
boolean	equals(nullable Object o)
Object	get(nullable Object key)
int	hashCode()
boolean	isEmpty()
Set	keySet()
Object	put(nullable Object key, nullable Object value)
void	putAll(Map t)
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

 

Field Detail

keySet

transient volatile Set keySet

values

transient volatile Collection values

AbstractMap

protected AbstractMap()

size

public int size()

Specified by:

size in interface Map

Specifications: (inherited)pure

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

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

    implies_that

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

containsValue

public boolean containsValue(nullable Object value)

Specified by:

containsValue in interface Map

Specifications: (inherited)pure

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

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 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 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:

     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;

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;

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

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

entrySet

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

equals

public boolean equals(nullable Object o)

Specified by:

equals in interface Map

Overrides:

equals in class Object

Specifications: (inherited)pure

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

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;

clone

protected Object clone()
                throws CloneNotSupportedException

Overrides:

clone in class Object

Throws:

CloneNotSupportedException

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