org.jmlspecs.samples.digraph
Class SearchableDigraph

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

public class SearchableDigraph

extends TransposableDigraph

Directed graphs that are searchable.

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
[spec_public] private  int	time

 

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

arcSet, nodeSet

 

Constructor Summary

SearchableDigraph()           Initialize this searchable digraph to be empty.

 

Model Method Summary

 

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

flipAll

 

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

OneMoreStep, reachSet

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	DFS()
void	DFSVisit(SearchableNode u)

 

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

transpose

 

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

 

Field Detail

time

private int time

Specifications: spec_public

SearchableDigraph

public SearchableDigraph()

Initialize this searchable digraph to be empty.

Specifications:

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

DFS

public void DFS()

Specifications:

public normal_behavior
assignable time, arcs, nodes;

DFSVisit

public void DFSVisit(SearchableNode u)

Specifications:

public normal_behavior
requires u != null&&u.color != null&&u.color == java.awt.Color.WHITE;
assignable time, arcs, u.discoverTime, u.color, u.predecessor, u.finishTime;
ensures u.color == java.awt.Color.BLACK&&u.discoverTime == \old(this.time+1)&&this.time > \old(this.time);