java.util
Class Dictionary

java.lang.Object
  java.util.Dictionary

Direct Known Subclasses:

Hashtable

public abstract class Dictionary

extends Object

Class Specifications

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

 

Ghost Field Summary
Class	elementType
Class	keyType

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Constructor Summary

Dictionary()

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
abstract  Enumeration	elements()
abstract  Object	get(nullable Object key)
abstract  boolean	isEmpty()
abstract  Enumeration	keys()
abstract  Object	put(nullable Object key, nullable Object value)
abstract  Object	remove(nullable Object key)
abstract  int	size()

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Ghost Field Detail

keyType

public Class keyType

elementType

public Class elementType

Dictionary

public Dictionary()

Specifications: pure

size

public abstract int size()

Specifications:

assignable \nothing;

isEmpty

public abstract boolean isEmpty()

Specifications:

assignable \nothing;

keys

public abstract Enumeration keys()

Specifications: non_null

assignable \nothing;

elements

public abstract Enumeration elements()

Specifications: non_null

assignable \nothing;

get

public abstract Object get(nullable Object key)

Specifications: nullable

requires key != null;
assignable \nothing;

put

public abstract Object put(nullable Object key,
                           nullable Object value)

Specifications: nullable

requires key != null;
requires value != null;

remove

public abstract Object remove(nullable Object key)

Specifications: nullable

requires key != null;