mjc

org.multijava.util
Class MjcHashRelation

java.lang.Object
  extended byorg.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
Constructor Detail

MjcHashRelation

public MjcHashRelation()

    modifiable theRelation;
    ensures theRelation.isEmpty();
 


MjcHashRelation

public MjcHashRelation(int size)

    modifiable theRelation;
    ensures theRelation.isEmpty();
 

Method Detail

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

mjc

mjc is Copyright (C) 2000-2004 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. mjc is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.