Package org.jmlspecs.samples.digraph

This package contains samples of JML specifications for directed graphs.

See:
Description

Interface Summary

NodeType

Class Summary

Arc	Directed arcs for directed graphs.
Arc_JML_Test	Automatically-generated test driver for JML and JUnit based testing of Arc.
Arc_JML_Test.OneTest	A JUnit test object that can run a single test method.
Arc_JML_Test.TestArc	Test for the Arc contructor.
Arc_JML_Test.TestClone	Test for the clone method.
Arc_JML_Test.TestEquals	Test for the equals method.
Arc_JML_Test.TestFlip	Test for the flip method.
Arc_JML_Test.TestGetSource	Test for the getSource method.
Arc_JML_Test.TestGetTarget	Test for the getTarget method.
Arc_JML_Test.TestHashCode	Test for the hashCode method.
Arc_JML_Test.TestSetSource	Test for the setSource method.
Arc_JML_Test.TestSetTarget	Test for the setTarget method.
Arc_JML_Test.TestToString	Test for the toString method.
Arc_JML_TestData	Supply test data for the JML and JUnit based testing of Arc.
ArcType
Digraph	Directed graphs.
NodeType_JML_Test	Automatically-generated test driver for JML and JUnit based testing of NodeType.
NodeType_JML_Test.OneTest	A JUnit test object that can run a single test method.
NodeType_JML_Test.TestClone	Test for the clone method.
NodeType_JML_Test.TestEquals	Test for the equals method.
NodeType_JML_Test.TestHashCode	Test for the hashCode method.
NodeType_JML_TestData	Supply test data for the JML and JUnit based testing of NodeType.
SearchableDigraph	Directed graphs that are searchable.
SearchableDigraph_JML_Test	Automatically-generated test driver for JML and JUnit based testing of SearchableDigraph.
SearchableDigraph_JML_Test.OneTest	A JUnit test object that can run a single test method.
SearchableDigraph_JML_Test.TestAddArc	Test for the addArc method.
SearchableDigraph_JML_Test.TestAddNode	Test for the addNode method.
SearchableDigraph_JML_Test.TestDFS	Test for the DFS method.
SearchableDigraph_JML_Test.TestDFSVisit	Test for the DFSVisit method.
SearchableDigraph_JML_Test.TestIsAPath	Test for the isAPath method.
SearchableDigraph_JML_Test.TestIsArc	Test for the isArc method.
SearchableDigraph_JML_Test.TestIsNode	Test for the isNode method.
SearchableDigraph_JML_Test.TestRemoveArc	Test for the removeArc method.
SearchableDigraph_JML_Test.TestRemoveNode	Test for the removeNode method.
SearchableDigraph_JML_Test.TestSearchableDigraph	Test for the SearchableDigraph contructor.
SearchableDigraph_JML_Test.TestToString	Test for the toString method.
SearchableDigraph_JML_Test.TestTranspose	Test for the transpose method.
SearchableDigraph_JML_Test.TestUnconnected	Test for the unconnected method.
SearchableDigraph_JML_TestData	Supply test data for the JML and JUnit based testing of SearchableDigraph.
SearchableNode	Nodes for searchable graphs.
SearchableNode_JML_Test	Automatically-generated test driver for JML and JUnit based testing of SearchableNode.
SearchableNode_JML_Test.OneTest	A JUnit test object that can run a single test method.
SearchableNode_JML_Test.TestClone	Test for the clone method.
SearchableNode_JML_Test.TestEquals	Test for the equals method.
SearchableNode_JML_Test.TestGetColor	Test for the getColor method.
SearchableNode_JML_Test.TestGetDiscoverTime	Test for the getDiscoverTime method.
SearchableNode_JML_Test.TestGetFinishTime	Test for the getFinishTime method.
SearchableNode_JML_Test.TestGetPredecessor	Test for the getPredecessor method.
SearchableNode_JML_Test.TestGetValue	Test for the getValue method.
SearchableNode_JML_Test.TestHashCode	Test for the hashCode method.
SearchableNode_JML_Test.TestSearchableNode	Test for the SearchableNode contructor.
SearchableNode_JML_Test.TestSetValue	Test for the setValue method.
SearchableNode_JML_Test.TestToString	Test for the toString method.
SearchableNode_JML_TestData	Supply test data for the JML and JUnit based testing of SearchableNode.
TestSuite	This class is automatically generated using org.multijava.util.testing.Main and is used to group a collection of JUnit tests for the local package and perhaps some subpackages.
TestSuite.TestSuite$1
TransposableDigraph	Transposable directed graphs.
TransposableDigraph_JML_Test	Automatically-generated test driver for JML and JUnit based testing of TransposableDigraph.
TransposableDigraph_JML_Test.OneTest	A JUnit test object that can run a single test method.
TransposableDigraph_JML_Test.TestAddArc	Test for the addArc method.
TransposableDigraph_JML_Test.TestAddNode	Test for the addNode method.
TransposableDigraph_JML_Test.TestIsAPath	Test for the isAPath method.
TransposableDigraph_JML_Test.TestIsArc	Test for the isArc method.
TransposableDigraph_JML_Test.TestIsNode	Test for the isNode method.
TransposableDigraph_JML_Test.TestRemoveArc	Test for the removeArc method.
TransposableDigraph_JML_Test.TestRemoveNode	Test for the removeNode method.
TransposableDigraph_JML_Test.TestToString	Test for the toString method.
TransposableDigraph_JML_Test.TestTransposableDigraph	Test for the TransposableDigraph contructor.
TransposableDigraph_JML_Test.TestTranspose	Test for the transpose method.
TransposableDigraph_JML_Test.TestUnconnected	Test for the unconnected method.
TransposableDigraph_JML_TestData	Supply test data for the JML and JUnit based testing of TransposableDigraph.
TransposableNode	Nodes for transposable directed graphs.
TransposableNode_JML_Test	Automatically-generated test driver for JML and JUnit based testing of TransposableNode.
TransposableNode_JML_Test.OneTest	A JUnit test object that can run a single test method.
TransposableNode_JML_Test.TestClone	Test for the clone method.
TransposableNode_JML_Test.TestEquals	Test for the equals method.
TransposableNode_JML_Test.TestGetValue	Test for the getValue method.
TransposableNode_JML_Test.TestHashCode	Test for the hashCode method.
TransposableNode_JML_Test.TestSetValue	Test for the setValue method.
TransposableNode_JML_Test.TestToString	Test for the toString method.
TransposableNode_JML_Test.TestTransposableNode	Test for the TransposableNode contructor.
TransposableNode_JML_TestData	Supply test data for the JML and JUnit based testing of TransposableNode.
ValueNode	Nodes with values

Package org.jmlspecs.samples.digraph Description

This package contains samples of JML specifications for directed graphs. It contains two sets of examples.

The type ArcType, NodeType, and Digraph are used in the preliminary design document. These were mostly written originally by Albert Baker.

The remaining types (that are not about testing) are perhaps better examples of directed graphs in practice. These were written and implemented by Katie Becker, under the supervision of Gary T. Leavens. Their implentations were later refined by Gary T. Leavens.