java.util
Interface Map.Entry

All Known Implementing Classes:

AbstractMap.SimpleEntry, HashMap.Entry, Launcher.ToolIteratorPair, TreeMap.Entry

Enclosing interface:

Map

public static interface Map.Entry

Class Specifications

Specifications inherited from class Object

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

Model Field Summary
[instance]  Object	abstractKey
[instance]  Object	abstractValue

 

Ghost Field Summary
[instance]  boolean	containsNull           True iff we are allowed to contain null:

 

Method Summary
boolean	equals(nullable Object o)
Object	getKey()
Object	getValue()
int	hashCode()
Object	setValue(Object value)

 

Model Field Detail

abstractKey

public Object abstractKey

Specifications: instance nullable
datagroup contains: java.util.HashMap$Entry.key org.multijava.launcher.Launcher$ToolIteratorPair.toolName

abstractValue

public Object abstractValue

Specifications: instance nullable
datagroup contains: java.util.HashMap$Entry.value org.multijava.launcher.Launcher$ToolIteratorPair.launcher

containsNull

public boolean containsNull

True iff we are allowed to contain null:

Specifications: instance

getKey

public Object getKey()

Specifications: pure nullable

public normal_behavior
ensures \result == this.abstractKey;

getValue

public Object getValue()

Specifications: pure nullable

public normal_behavior
ensures \result == this.abstractValue;

setValue

public Object setValue(Object value)

Specifications:

public behavior
assignable this.abstractValue;
ensures \result == \old(this.abstractValue);
ensures this.abstractValue == value;
signals_only java.lang.NullPointerException, java.lang.UnsupportedOperationException, java.lang.ClassCastException, java.lang.IllegalArgumentException;
signals (java.lang.NullPointerException) \not_modified(this.abstractValue)&&(this.abstractValue == null)&&!this.containsNull;
signals (java.lang.UnsupportedOperationException) \not_modified(this.abstractValue)&&(* if the map's put operation is not supported *);
signals (java.lang.ClassCastException) \not_modified(this.abstractValue)&&(* \typeof(abstractValue) is incompatible with the valueType of this map *);
signals (java.lang.IllegalArgumentException) \not_modified(this.abstractValue)&&(* if some aspect of value is not allowed in the map *);

equals

public boolean equals(nullable Object o)

Overrides:

equals in class Object

Specifications: pure

     also

public normal_behavior
requires o instanceof java.util.Map.Entry;
ensures \result == (org.jmlspecs.models.JMLNullSafe.equals(((java.util.Map.Entry)o).abstractKey,this.abstractKey)&&org.jmlspecs.models.JMLNullSafe.equals(((java.util.Map.Entry)o).abstractValue,this.abstractValue));

     also

public normal_behavior
requires !(o instanceof java.util.Map.Entry);
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;