org.multijava.util
Class MjcHashRelation

java.lang.Object
  org.multijava.util.MjcHashRelation

public final class MjcHashRelation

extends Object

This class is used to map a key to a sequence of values, the image of the key. This allows a key to map to multiple values, i.e., this ADT represents a relation rather than a function.

Field Summary
private  HashMap	theMap

 

Constructor Summary

MjcHashRelation()            modifiable theRelation; ensures theRelation.isEmpty();

MjcHashRelation(int size)            modifiable theRelation; ensures theRelation.isEmpty();

 

Method Summary
void	clear()            modifiable theRelation; ensures theRelation.isEmpty();
boolean	containsKey(Object key)            requires key !
boolean	containsValue(Object value)           Returns true if there exists a key such that theRelation.elementImage(key).has( value ), otherwise it returns false.
protected static int	findValue(ArrayList theList, Comparable value)           This method is used to place the elements in theList in order.
Comparable	get(Object key)           Returns the least value in the set of values mapped to by the given key (if the image of the given key has been sorted), or null if this key is not in the domain of the theRelation.
Collection	getImage(Object key)           Returns the collection of values mapped to by the given key, or null if this key is not in the domain of the theRelation.
Comparable	getNextValue(Object key, Comparable value)
static Comparable	getNextValueFromN(MjcHashRelation[] rels, Object key, Comparable value)
Comparable	put(Object key, Comparable value)           Adds value to the set of values in the image of the given key.
Collection	putImage(Object key, Collection image)           Adds a mapping from the given key to the given image.
Object	remove(Object key)
Object	remove(Object key, Comparable value)           requires key !
int	size()            ensures \result == theRelation.domain().int_size();
boolean	sortImage(Object key)

 

Methods inherited from class java.lang.Object

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

 

Field Detail

theMap

private HashMap theMap

MjcHashRelation

public MjcHashRelation()

    modifiable theRelation;
    ensures theRelation.isEmpty();
 

MjcHashRelation

public MjcHashRelation(int size)

    modifiable theRelation;
    ensures theRelation.isEmpty();
 

clear

public void clear()

    modifiable theRelation;
    ensures theRelation.isEmpty();
 

size

public int size()

    ensures \result == theRelation.domain().int_size();
 

containsKey

public boolean containsKey(Object key)

    requires key != null;
    ensures \result == theRelation.isDefinedAt(key);
 

containsValue

public boolean containsValue(Object value)

Returns true if there exists a key such that theRelation.elementImage(key).has( value ), otherwise it returns false.

    requires value != null 
        && (\exists Object key; key != null;
                    theRelation.elementImage(key).has(value));
    ensures \result == true;
  also
    requires value != null 
        && (\forall Object key; key != null;
                    ! theRelation.elementImage(key).has(value));
    ensures \result == false;
 

remove

public Object remove(Object key)

remove

public Object remove(Object key,
                     Comparable value)

requires key != null && value != null && theRelation.isDefinedAt(key) modifiable theRelation; ensures theRelation == \old(theRelation).removeFromDomain(key).add(key, value); && \result == null;

get

public Comparable get(Object key)

Returns the least value in the set of values mapped to by the given key (if the image of the given key has been sorted), or null if this key is not in the domain of the theRelation.

    requires key != null && theRelation.isDefinedAt(key);
    ensures (* \result == the first element in the list of values 
                          in theRelation.elementImage(key) *);
  also
    requires key != null && ! theRelation.isDefinedAt(key);
    ensures \result == null;
 

getImage

public Collection getImage(Object key)

Returns the collection of values mapped to by the given key, or null if this key is not in the domain of the theRelation.

    requires key != null && theRelation.isDefinedAt(key);
    ensures \result.equals(theRelation.elementImage(key));
  also
    requires key != null && ! theRelation.isDefinedAt(key);
    ensures \result == null;
 

put

public Comparable put(Object key,
                      Comparable value)

Adds value to the set of values in the image of the given key.

    requires key != null && value != null 
        && ! (\exists Object aValue; aValue != null; 
                      theRelation.elementImage(key).has( aValue )
                      && aValue == value);
    requires_redundantly (* the (key, value) pair is not already in 
                            theRelation *);
    modifiable theRelation;
    ensures theRelation.equals( \old(theRelation).add(key, value) )
         && \old(theRelation).elementImage(key).has(\result);
  also
    requires key != null && value != null 
        && (\exists Object aValue; aValue != null; 
                    theRelation.elementImage(key).has( aValue )
                    && aValue == value);
    requires_redundantly (* the (key, value) pair is already in 
                            theRelation *);
    ensures \result == null;
 

putImage

public Collection putImage(Object key,
                           Collection image)

Adds a mapping from the given key to the given image.

 requires key != null && image != null &&
          (\forall Object o; image.contains(o); o instanceof Comparable);
 

sortImage

public boolean sortImage(Object key)

getNextValue

public Comparable getNextValue(Object key,
                               Comparable value)

getNextValueFromN

public static Comparable getNextValueFromN(MjcHashRelation[] rels,
                                           Object key,
                                           Comparable value)

findValue

protected static int findValue(ArrayList theList,
                               Comparable value)

This method is used to place the elements in theList in order. Returns the index where value is located in theList or where value could be inserted (by subtracting the size of theList) if it is not already in the list.

Parameters:

value - the object being searched for