org.jmlspecs.samples.digraph
Class TransposableDigraph

java.lang.Object
  org.jmlspecs.samples.digraph.Digraph
      org.jmlspecs.samples.digraph.TransposableDigraph

Direct Known Subclasses:

SearchableDigraph

public class TransposableDigraph

extends Digraph

Transposable directed graphs.

Author:

Katie Becker, Gary T. Leavens

Class Specifications

Specifications inherited from class Digraph

private invariant_redundantly this.nodeSet != null; private invariant ( \forall java.lang.Object e; this.nodeSet.contains(e); e != null&&e instanceof org.jmlspecs.samples.digraph.NodeType); private invariant_redundantly this.arcSet != null; private invariant ( \forall java.lang.Object e; this.arcSet.contains(e); e != null&&e instanceof org.jmlspecs.samples.digraph.Arc); public invariant_redundantly this.nodes != null; public invariant ( \forall org.jmlspecs.models.JMLType n; this.nodes.has(n); n instanceof org.jmlspecs.samples.digraph.NodeType); public invariant_redundantly this.arcs != null; public invariant ( \forall org.jmlspecs.models.JMLType a; this.arcs.has(a); a instanceof org.jmlspecs.samples.digraph.ArcType); public invariant ( \forall org.jmlspecs.samples.digraph.ArcType a; this.arcs.has(a); this.nodes.has(a.from)&&this.nodes.has(a.to)); private represents nodes <- org.jmlspecs.models.JMLValueSet.convertFrom(this.nodeSet); private represents arcs <- this.arcAbstractValue(this.arcSet);

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary

 

Model fields inherited from class org.jmlspecs.samples.digraph.Digraph

arcs, nodes

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary

 

Fields inherited from class org.jmlspecs.samples.digraph.Digraph

arcSet, nodeSet

 

Constructor Summary

TransposableDigraph()           Initialize this transposable digraph to be empty.

 

Model Method Summary
JMLValueSet	flipAll(JMLValueSet s)           Return a set with each edge inverted.

 

Model methods inherited from class org.jmlspecs.samples.digraph.Digraph

OneMoreStep, reachSet

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	transpose()           Transpose this graph by inverting the direction of all its edges.

 

Methods inherited from class org.jmlspecs.samples.digraph.Digraph

addArc, addNode, isAPath, isArc, isNode, reachSet, removeArc, removeNode, toString, unconnected

 

Methods inherited from class java.lang.Object

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

 

Constructor Detail

TransposableDigraph

public TransposableDigraph()

Initialize this transposable digraph to be empty.

Specifications:

public normal_behavior
assignable nodes, arcs;
ensures this.nodes.isEmpty()&&this.arcs.isEmpty();

flipAll

public JMLValueSet flipAll(JMLValueSet s)

Return a set with each edge inverted.

Specifications: pure

transpose

public void transpose()

Transpose this graph by inverting the direction of all its edges.

Specifications:

public normal_behavior
assignable arcs;
ensures this.nodes.equals(\old(this.nodes));
ensures this.arcs.equals(this.flipAll(\old(this.arcs)));