java.util
Class TreeMap

java.lang.Object
  java.util.AbstractMap
      java.util.TreeMap

All Implemented Interfaces:

Cloneable, Map, Serializable, SortedMap

public class TreeMap

extends AbstractMap

implements SortedMap, Cloneable, Serializable

JML's specification of java.util.TreeMap.

Version:

$Revision: 1.14 $

Author:

Katie Becker, Gary T. Leavens

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	TreeMap.Entry

 

Nested classes inherited from class java.util.AbstractMap

AbstractMap.SimpleEntry

 

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Model fields inherited from interface java.util.SortedMap

firstKey, lastKey

 

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

 

Fields inherited from class java.util.AbstractMap

keySet, values

 

Constructor Summary

TreeMap()

TreeMap(Comparator c)

TreeMap(Map m)

TreeMap(SortedMap 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	addAllForTreeSet(SortedSet set, Object defaultVal)
void	clear()
Object	clone()
Comparator	comparator()
boolean	containsKey(nullable Object key)
boolean	containsValue(nullable Object value)
Set	entrySet()
Object	firstKey()
Object	get(nullable Object key)
SortedMap	headMap(Object toKey)
Set	keySet()
Object	lastKey()
Object	put(nullable Object key, nullable Object value)
void	putAll(Map map)
(package private)  void	readTreeSet(int size, ObjectInputStream s, Object defaultVal)
Object	remove(nullable Object key)
int	size()
SortedMap	subMap(Object fromKey, Object toKey)
SortedMap	tailMap(Object fromKey)
Collection	values()

 

Methods inherited from class java.util.AbstractMap

equals, hashCode, isEmpty, toString

 

Methods inherited from class java.lang.Object

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

 

Methods inherited from interface java.util.Map

equals, hashCode, isEmpty

 

Constructor Detail

TreeMap

public TreeMap()

Specifications: pure

private normal_behavior
assignable theMap;
ensures this.theMap != null&&this.theMap.isEmpty();

TreeMap

public TreeMap(Comparator c)

Specifications: pure

private normal_behavior
assignable theMap;
ensures this.theMap != null&&this.theMap.isEmpty();

TreeMap

public TreeMap(SortedMap m)

Specifications: pure

private normal_behavior
requires m != null;
assignable theMap;
ensures this.theMap != null;
ensures org.jmlspecs.models.JMLEqualsSet.convertFrom(m.entrySet()).equals(this.theMap);

TreeMap

public TreeMap(Map m)

Specifications: pure

private normal_behavior
requires m != null;
assignable theMap;
ensures this.theMap != null;
ensures org.jmlspecs.models.JMLEqualsSet.convertFrom(m.entrySet()).equals(this.theMap);

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;

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

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

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

comparator

public Comparator comparator()

Specified by:

comparator in interface SortedMap

Specifications: (inherited)pure

Specifications inherited from overridden method in interface SortedMap:
       pure

public normal_behavior
ensures true;

firstKey

public Object firstKey()

Specified by:

firstKey in interface SortedMap

Specifications: (inherited)pure

Specifications inherited from overridden method in interface SortedMap:
       pure

public behavior
assignable \nothing;
ensures \result .equals(this.firstKey);
signals_only java.util.NoSuchElementException;
signals (java.util.NoSuchElementException) this.isEmpty();

lastKey

public Object lastKey()

Specified by:

lastKey in interface SortedMap

Specifications: (inherited)pure

Specifications inherited from overridden method in interface SortedMap:
       pure

public behavior
assignable \nothing;
ensures \result .equals(this.lastKey);
signals_only java.util.NoSuchElementException;
signals (java.util.NoSuchElementException) this.isEmpty();

putAll

public void putAll(Map map)

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;

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

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

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;

clone

public Object clone()

Overrides:

clone in class AbstractMap

Specifications: pure

     also

public normal_behavior
ensures \result instanceof java.util.TreeMap&&\fresh(\result )&&((java.util.TreeMap)\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]);

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

subMap

public SortedMap subMap(Object fromKey,
                        Object toKey)

Specified by:

subMap in interface SortedMap

Specifications: (inherited)pure

Specifications inherited from overridden method subMap(Object fromKey, Object toKey) in interface SortedMap:
       pure

public behavior
assignable \nothing;
ensures (\result .firstKey.equals(this.firstKey));
ensures \result != null;
signals_only java.lang.ClassCastException, java.lang.IllegalArgumentException, java.lang.NullPointerException;
signals (java.lang.ClassCastException) (* \typeof(fromKey) or \typeof(toKey) is incompatible with this map's comparator *);
signals (java.lang.IllegalArgumentException) (* fromKey > toKey || fromKey or toKey is not within the domain of the SortedMap *);
signals (java.lang.NullPointerException) (fromKey == null||toKey == null)&&!this.containsNull;

headMap

public SortedMap headMap(Object toKey)

Specified by:

headMap in interface SortedMap

Specifications: (inherited)pure

Specifications inherited from overridden method headMap(Object toKey) in interface SortedMap:
       pure

public behavior
assignable \nothing;
ensures (\result .firstKey.equals(this.firstKey));
ensures \result != null;
signals_only java.lang.ClassCastException, java.lang.IllegalArgumentException, java.lang.NullPointerException;
signals (java.lang.ClassCastException) (* \typeof(toKey) is incompatible with with this map's comparator *);
signals (java.lang.IllegalArgumentException) (* toKey is not within the domain of the SortedMap *);
signals (java.lang.NullPointerException) toKey == null&&!this.containsNull;

tailMap

public SortedMap tailMap(Object fromKey)

Specified by:

tailMap in interface SortedMap

Specifications: (inherited)pure

Specifications inherited from overridden method tailMap(Object fromKey) in interface SortedMap:
       pure

public behavior
assignable \nothing;
ensures \result != null;
signals_only java.lang.ClassCastException, java.lang.IllegalArgumentException, java.lang.NullPointerException;
signals (java.lang.ClassCastException) (* \typeof(fromKey) is incompatible with this map's comparator *);
signals (java.lang.IllegalArgumentException) (* fromKey is not within the domain of the SortedMap *);
signals (java.lang.NullPointerException) fromKey == null&&!this.containsNull;

readTreeSet

void readTreeSet(int size,
                 ObjectInputStream s,
                 Object defaultVal)
           throws IOException,
                  ClassNotFoundException

Throws:

IOException

ClassNotFoundException

addAllForTreeSet

void addAllForTreeSet(SortedSet set,
                      Object defaultVal)