JML

java.util
Class HashMap.Entry

java.lang.Object
  extended byjava.util.HashMap.Entry
All Implemented Interfaces:
Map.Entry
Enclosing class:
HashMap

static class HashMap.Entry
extends Object
implements Map.Entry


Class Specifications
represents abstractKey <- this.key;
represents abstractValue <- this.value;

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Model Field Summary
 
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
 
Model fields inherited from interface java.util.Map.Entry
abstractKey, abstractValue
 
Ghost Field Summary
 
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
 
Ghost fields inherited from interface java.util.Map.Entry
containsNull
 
Field Summary
(package private)  int hash
           
(package private)  Object key
           
(package private)  HashMap.Entry next
           
(package private)  Object value
           
 
Constructor Summary
(package private) HashMap.Entry(int h, Object k, Object v, HashMap.Entry n)
           
 
Model Method Summary
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
 boolean equals(nullable Object o)
           
 Object getKey()
           
 Object getValue()
           
 int hashCode()
           
(package private)  void recordAccess(HashMap m)
           
(package private)  void recordRemoval(HashMap m)
           
 Object setValue(Object newValue)
           
 String toString()
           
 
Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
 

Field Detail

key

final Object key
Specifications:
is in groups: abstractKey

value

Object value
Specifications:
is in groups: abstractValue

hash

final int hash

next

HashMap.Entry next
Constructor Detail

HashMap.Entry

HashMap.Entry(int h,
              Object k,
              Object v,
              HashMap.Entry n)
Specifications:
assignable abstractKey, abstractValue;
ensures this.abstractKey == k&&this.abstractValue == v;
Method Detail

getKey

public Object getKey()
Specified by:
getKey in interface Map.Entry
Specifications: (inherited)pure
Specifications inherited from overridden method in interface Entry:
       pure nullable
public normal_behavior
ensures \result == this.abstractKey;

getValue

public Object getValue()
Specified by:
getValue in interface Map.Entry
Specifications: (inherited)pure
Specifications inherited from overridden method in interface Entry:
       pure nullable
public normal_behavior
ensures \result == this.abstractValue;

setValue

public Object setValue(Object newValue)
Specified by:
setValue in interface Map.Entry
Specifications inherited from overridden method setValue(Object value) in interface Entry:
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)
Specified by:
equals in interface Map.Entry
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 Entry:
       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;

hashCode

public int hashCode()
Specified by:
hashCode in interface Map.Entry
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 Entry:
       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;

recordAccess

void recordAccess(HashMap m)

recordRemoval

void recordRemoval(HashMap m)

JML

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.