org.jutil.java.collections
Class Mapping

java.lang.Object
  |
  +--org.jutil.java.collections.Mapping

All Implemented Interfaces:

CollectionOperator

public abstract class Mapping

extends java.lang.Object

implements CollectionOperator

A mapping of collections.

Mappings exchange an element for another element, calculated based on the original element. In relational algebra, this is projection.

That mapping is defined in the mapping(Object) method. The mapping of the collection happens through the invocation of the applyTo(Collection) method, or the applyTo(Collection, Collection) method which maps the first collection into the second.

The code it typically used as follows:

 new Mapping() {
   /oo
     o also public behavior
     o
     o post (* postconditions *);
     o/
   public Object mapping(Object element) {
     // mapping code
   }
 }.applyTo(collection);
 

Field Summary
static java.lang.String	CVS_REVISION

 

Constructor Summary

Mapping()

 

Method Summary
java.util.Collection	applyFromTo(java.util.Collection fromCollection, java.util.Collection toCollection)           Perform the mapping defined in public Object mapping(Object) on all elements in and put them in .
java.util.Collection	applyTo(java.util.Collection collection)           Perform the mapping defined in public Object mapping(Object) on .
abstract  java.lang.Object	mapping(java.lang.Object element)           The mapping to be applied to all elements of a collection.

 

Methods inherited from class java.lang.Object

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

 

Methods inherited from interface org.jutil.java.collections.CollectionOperator

isValidElement

 

Field Detail

CVS_REVISION

public static final java.lang.String CVS_REVISION

Mapping

public Mapping()

mapping

public abstract java.lang.Object mapping(java.lang.Object element)

The mapping to be applied to all elements of a collection.

Parameters:

element - The object the mapping should replace.

Specifications:

public behavior
requires isValidElement(element);
ensures ( \forall Object o1; ; ( \forall Object o2; (o2 != null)&&o2.equals(o1); mapping(o1).equals(mapping(o2))));

applyTo

public final java.util.Collection applyTo(java.util.Collection collection)
                                   throws java.util.ConcurrentModificationException

Perform the mapping defined in public Object mapping(Object) on . The contents of is changed to the mapping. The collection is also returned, so that further operations can be applied to it inline.

If the collection is a sorted set, make sure that the new elements are also Comparable, or that the Comparator is changed accordingly.

If the collection is a List, the order of the elements is preserved. The mapped element has the same position as the object it was mapped from.

Parameters:

collection - The collection to perform this mapping on. This can be null, in which case nothing happens.

Specifications:

public behavior
requires ( \forall Object o; collection.contains(o); isValidElement(o));
ensures ( \forall Object o; collection.contains(o); \result .contains(mapping(o)))&&( \forall Object o; \result .contains(o); ( \exists Object o2; collection.contains(o2); mapping(o2).equals(o)));
ensures collection.size() == \old(collection.size());
ensures \result == collection;
signals (ConcurrentModificationException) (* The collection was modified while mapping *);

applyFromTo

public final java.util.Collection applyFromTo(java.util.Collection fromCollection,
                                              java.util.Collection toCollection)
                                       throws java.util.ConcurrentModificationException

Perform the mapping defined in public Object mapping(Object) on all elements in and put them in . The contents of is not changed. is also returned, so that further operations can be applied to it inline.

If is a sorted set, make sure that the new elements are also Comparable, or that the Comparator is changed accordingly.

If is a List, the order of the elements is preserved. The mapped element has the same position in as the object it was mapped from in .

Parameters:

fromCollection - The collection which contains to elements to be mapped into the other collection. This can be null, in which case nothing happens.

toCollection - The collection into which the elements of are mapped. This can be null, in which case nothing happens.

Specifications:

public behavior
requires ( \forall Object o; fromCollection.contains(o); isValidElement(o));
ensures ( \forall Object o; fromCollection.contains(o); \result .contains(mapping(o)))&&( \forall Object o; toCollection.contains(o); ( \exists Object o2; fromCollection.contains(o2); o.equals(mapping(o2))));
ensures \result == toCollection;
signals (ConcurrentModificationException) (* The collection was modified while mapping *);