java.util
Interface Map

All Known Subinterfaces:

SortedMap

All Known Implementing Classes:

AbstractMap, HashMap, Hashtable, TreeMap

public interface Map

JML's specification of java.util.Map.

Version:

$Revision: 1.20 $

Author:

Katie Becker, Gary T. Leavens

Class Specifications

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

Specifications inherited from class Object

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

Model Field Summary
[instance]  JMLEqualsSet	theMap

 

Ghost Field Summary
[instance]  boolean	containsNull           True iff we are allowed to contain null keys and values.

 

Model Method Summary
boolean	contains(Object key, Object value)
boolean	contains(Map.Entry e)
static boolean	nullequals(nullable Object o, nullable Object oo)

 

Method Summary
void	clear()
boolean	containsKey(nullable Object key)
boolean	containsValue(nullable Object value)
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()
Collection	values()

 

Model Field Detail

theMap

public JMLEqualsSet theMap

Specifications: instance non_null
is in groups: objectState
datagroup contains: java.util.SortedMap.firstKey java.util.SortedMap.lastKey

containsNull

public boolean containsNull

True iff we are allowed to contain null keys and values.

Specifications: instance

nullequals

public static boolean nullequals(nullable Object o,
                                 nullable Object oo)

Specifications: pure

public normal_behavior
ensures \result == (o == oo||(o != null&&oo != null&&o.equals(oo)));

contains

public boolean contains(Map.Entry e)

Specifications: pure

public normal_behavior
requires e != null;
ensures \result <==> this.contains(e.getKey(),e.getValue());

contains

public boolean contains(Object key,
                        Object value)

Specifications: pure

size

public int size()

Specifications: pure

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

    implies_that

ensures \result >= 0;

isEmpty

public boolean isEmpty()

Specifications: pure

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

    implies_that

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

containsKey

public boolean containsKey(nullable Object key)

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

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

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

Specifications:

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)

Specifications:

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)

Specifications:

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

Specifications:

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

Specifications: pure

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

values

public Collection values()

Specifications: pure

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

entrySet

public Set entrySet()

Specifications: pure

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

equals

public boolean equals(nullable Object o)

Overrides:

equals in class Object

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

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 ;

hashCode

public int hashCode()

Overrides:

hashCode in class Object

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