001: package java.util;
002:
003: import java.io.IOException;
004: import java.io.ObjectInputStream;
005: import java.io.ObjectOutputStream;
006: import java.io.Serializable;
007:
008: public class HashMap extends AbstractMap implements Map, Cloneable,
009: Serializable {
010:
011: //@ public model int initialCapacity;
012:
013: static final int DEFAULT_CAPACITY = 11;
014: static final float DEFAULT_LOAD_FACTOR = 0.75f;
015: final float loadFactor;
016: transient HashEntry[] buckets;
017: transient int modCount;
018: transient int size;
019:
020: static class HashEntry extends AbstractMap.BasicMapEntry {
021: HashEntry next;
022:
023: HashEntry(Object key, Object value) {
024: }
025:
026: void access() {
027: }
028:
029: Object cleanup() {
030: }
031: }
032:
033: public HashMap() {
034: }
035:
036: /*@ public normal_behavior
037: @ requires m != null;
038: @ assignable theMap, initialCapacity, loadFactor;
039: @ ensures theMap.equals(m.theMap);
040: @*/
041: public HashMap(Map m) {
042: }
043:
044: /*@ public normal_behavior
045: @ assignable theMap, this.initialCapacity, this.loadFactor;
046: @ ensures theMap != null && theMap.isEmpty();
047: @ ensures this.initialCapacity == initialCapacity;
048: @*/
049: public HashMap(int initialCapacity) {
050: }
051:
052: /*@ public normal_behavior
053: @ requires initialCapacity >= 0;
054: @ assignable theMap, this.initialCapacity, this.loadFactor;
055: @ ensures theMap != null && theMap.isEmpty();
056: @ ensures this.initialCapacity == initialCapacity
057: @ && this.loadFactor == loadFactor;
058: @*/
059: public HashMap(int initialCapacity, float loadFactor) {
060: }
061:
062: public int size() {
063: }
064:
065: public boolean isEmpty() {
066: }
067:
068: public Object get(Object key) {
069: }
070:
071: public boolean containsKey(Object key) {
072: }
073:
074: public Object put(Object key, Object value) {
075: }
076:
077: public void putAll(Map m) {
078: }
079:
080: public Object remove(Object key) {
081: }
082:
083: public void clear() {
084: }
085:
086: public boolean containsValue(Object value) {
087: }
088:
089: /*@ also
090: @ public normal_behavior
091: @ assignable \nothing;
092: @ ensures \result instanceof Map && \fresh(\result)
093: @ && ((Map)\result).equals(this);
094: @ ensures_redundantly \result != this;
095: @*/
096: public Object clone() {
097: }
098:
099: public Set keySet() {
100: }
101:
102: public Collection values() {
103: }
104:
105: public Set entrySet() {
106: }
107:
108: void addEntry(Object key, Object value, int idx, boolean callRemove) {
109: }
110:
111: final HashEntry getEntry(Object o) {
112: }
113:
114: final int hash(Object key) {
115: }
116:
117: Iterator iterator(int type) {
118: }
119:
120: void putAllInternal(Map m) {
121: }
122:
123: private void rehash() {
124: }
125:
126: private void writeObject(ObjectOutputStream s) throws IOException {
127: }
128:
129: private void readObject(ObjectInputStream s) throws IOException,
130: ClassNotFoundException {
131: }
132:
133: private final class HashIterator implements Iterator {
134: HashIterator(int type) {
135: }
136:
137: public boolean hasNext() {
138: }
139:
140: public Object next() {
141: }
142:
143: public void remove() {
144: }
145: }
146: }
|