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.

Version:

$Revision: 1.12 $

Author:

Jan Dockx, Marko van Dooren

Field Summary

static java.lang.String

CVS_REVISION

Constructor Summary

TransitiveClosure()

Method Summary

java.util.Set	closure(java.lang.Object startNode) // The given node may not be null. pre startNode != null ; post \result.equals(closureFromAll(new Singleton(o))); signals (ConcurrentModificationException) (* The collection was modified while calculating the tranitive closure.
java.util.Set	closureFromAll(java.util.Set startSet) // The given set may not be null pre startSet != null; // The given set may not contain null references. pre (\forall Object o ; startSet.contains(o) ; o != null); // The result is effective. post \result != null // The transitive closure is the set of all nodes that can be reached from // a start set of nodes via connections defined by // public Set getConnectedNodes(Object node). post isNaiveClosure(startSet, \result); // Least Fixed Point post (\forall Set cn; (cn != null) && isNaiveClosure(startSet, cn); (\result.size() <= cn.size())); post_redundantly (\forall Object o; \result.contains(o); o != null); signals (ConcurrentModificationException) (* The collection was modified while calculating the tranitive closure.
abstract java.util.Set	getConnectedNodes(java.lang.Object node) // The given node may not be null pre node != null; // Never returns null. post \result != null; // Never contains null. post (\forall Object o; \result.contains(o); o != null);
boolean	isNaiveClosure(java.util.Set startSet, java.util.Set naiveClosureSet) pre startSet != null pre naiveClosureSet != null post \result == (\forall Object o; startSet.contains(o); (naiveClosureSet.contains(o) && (\exists Set ccn; isNaiveClosure(getConnectedNodes(o), ccn)); naiveClosureSet.containsAll(ccn))); 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

Constructor Detail

TransitiveClosure

public TransitiveClosure()

Method Detail

getConnectedNodes

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

// The given node may not be null
pre node != null;

// Never returns null.
post \result != null;
// Never contains null.
post (\forall Object o; \result.contains(o); o != null);

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.

isNaiveClosure

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

pre startSet != null
pre naiveClosureSet != null
post \result == (\forall Object o; startSet.contains(o);
(naiveClosureSet.contains(o) &&
(\exists Set ccn; isNaiveClosure(getConnectedNodes(o), ccn));
naiveClosureSet.containsAll(ccn)));
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)

closureFromAll

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

// The given set may not be null
pre startSet != null;
// The given set may not contain null references.
pre (\forall Object o ; startSet.contains(o) ; o != null);

// The result is effective.
post \result != null
// The transitive closure is the set of all nodes that can be reached from
// a start set of nodes via connections defined by
// public Set getConnectedNodes(Object node).
post isNaiveClosure(startSet, \result);
// Least Fixed Point
post (\forall Set cn;
(cn != null) && isNaiveClosure(startSet, cn);
(\result.size() <= cn.size()));
post_redundantly (\forall Object o; \result.contains(o); o != null);

signals (ConcurrentModificationException)
(* The collection was modified while calculating the tranitive closure. *);

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.

closure

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

// The given node may not be null.
pre startNode != null ;

post \result.equals(closureFromAll(new Singleton(o)));

signals (ConcurrentModificationException)
(* The collection was modified while calculating the tranitive closure. *);

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

Parameters:

startNode - The node to start the transitive closure from.