JML

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.


JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.