org.jutil.java.collections
Class TransitiveClosure

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

public abstract class TransitiveClosure

extends java.lang.Object

An operator that calculates the transitive closure of a graph of objects.

Objects of this class calculate the transitive closure of a graph, defined by public Set getConnectedNodes(Object node), starting from a set of nodes or a single start node.

Field Summary
static java.lang.String	CVS_REVISION

 

Constructor Summary

TransitiveClosure()

 

Method Summary
java.util.Set	closure(java.lang.Object startNode)           The transitive closure, starting from , defined by public Set getConnectedNodes(Object node).
java.util.Set	closureFromAll(java.util.Set startSet)           The transitive closure, starting from , defined by public Set getConnectedNodes(Object node).
abstract  java.util.Set	getConnectedNodes(java.lang.Object node)           This method needs to be implemented by subclasses, so that it returns the nodes connected to under the definition of the graph for which we want the transitive closure.
boolean	isNaiveClosure(java.util.Set startSet, java.util.Set naiveClosureSet)           Transitive closure is a recursive definition.

 

Methods inherited from class java.lang.Object

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

 

Field Detail

CVS_REVISION

public static final java.lang.String CVS_REVISION

TransitiveClosure

public TransitiveClosure()

getConnectedNodes

public abstract java.util.Set getConnectedNodes(java.lang.Object node)

This method needs to be implemented by subclasses, so that it returns the nodes connected to under the definition of the graph for which we want the transitive closure.

Parameters:

node - The node to get the connected nodes for.

Specifications:

requires node != null;
ensures \result != null;
ensures ( \forall Object o; \result .contains(o); o != null);

isNaiveClosure

public final boolean isNaiveClosure(java.util.Set startSet,
                                    java.util.Set naiveClosureSet)

Transitive closure is a recursive definition. The recursive post condition below returns true for all sets that contain the actual transitive closure, e.g., also for the set of all objects. We want the smallest set (Least Fixed Point) of the family of naive closure sets as result of closureFromAll. This extra requirement is added in the post condition of that method.

See Also:

closureFromAll(java.util.Set)

Specifications:

requires startSet != null;
requires naiveClosureSet != null;
ensures \result == ( \forall Object o; startSet.contains(o); (naiveClosureSet.contains(o)&&( \exists Set ccn; isNaiveClosure(getConnectedNodes(o),ccn); naiveClosureSet.containsAll(ccn))));

closureFromAll

public final java.util.Set closureFromAll(java.util.Set startSet)
                                   throws java.util.ConcurrentModificationException

The transitive closure, starting from , defined by public Set getConnectedNodes(Object node).

Parameters:

startSet - The set of nodes to start the transitive closure from. This set is not changed.

Specifications:

requires startSet != null;
requires ( \forall Object o; startSet.contains(o); o != null);
ensures \result != null;
ensures \fresh(\result );
ensures isNaiveClosure(startSet,\result );
ensures ( \forall Set cn; (cn != null)&&isNaiveClosure(startSet,cn); (\result .size() <= cn.size()));
ensures_redundantly ( \forall Object o; \result .contains(o); o != null);
signals (ConcurrentModificationException) (* The collection was modified while calculating the tranitive closure. *);

closure

public final java.util.Set closure(java.lang.Object startNode)
                            throws java.util.ConcurrentModificationException

The transitive closure, starting from , defined by public Set getConnectedNodes(Object node).

Parameters:

startNode - The node to start the transitive closure from.

Specifications:

requires startNode != null;
ensures \result .equals(closureFromAll(new Singleton(startNode)));
signals (ConcurrentModificationException) (* The collection was modified while calculating the tranitive closure. *);