All Packages  Class Hierarchy  This Package  Previous  Next  Index

Interface collections.UpdatableMap

public interface interface UpdatableMap

extends UpdatableCollection, Map

putAt(Object, Object)

Include the indicated pair in the Map If a different pair with the same key was previously held, it is replaced by the new pair.

removeAt(Object)

Remove the pair with the given key

replaceElement(Object, Object, Object)

Replace old pair with new pair with same key.

 public abstract void putAt(Object key,
                            Object element) throws IllegalElementException

Include the indicated pair in the Map If a different pair with the same key was previously held, it is replaced by the new pair.

Parameters:

key - the key for element to include

element - the element to include

Returns:

condition:

 includes(key, element) &&
 no spurious effects &&
 Version change iff !PREV(this).includesAt(key, element))
 

 public abstract void removeAt(Object key)

Remove the pair with the given key

Parameters:

key - the key

Returns:

condition:

 !includesKey(key)
 foreach (k in keys()) at(k).equals(PREV(this).at(k)) &&
 foreach (k in PREV(this).keys()) (!k.equals(key)) --> at(k).equals(PREV(this).at(k)) 
 (version() != PREV(this).version()) == 
 includesKey(key) !=  PREV(this).includesKey(key))
 

 public abstract void replaceElement(Object key,
                                     Object oldElement,
                                     Object newElement) throws IllegalElementException

Replace old pair with new pair with same key. No effect if pair not held. (This includes the case of having no effect if the key exists but is bound to a different value.)

Parameters:

key - the key for the pair to remove

oldElement - the existing element

newElement - the value to replace it with

Returns:

condition:

 !includesAt(key, oldElement) || includesAt(key, newElement);
 no spurious effects &&
 Version change iff PREV(this).includesAt(key, oldElement))
 

All Packages  Class Hierarchy  This Package  Previous  Next  Index