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_TestData	Supply test data for the JML and JUnit based testing of Arc.
ArcType
Digraph	Directed graphs.
NodeType_JML_TestData	Supply test data for the JML and JUnit based testing of NodeType.
SearchableDigraph	Directed graphs that are searchable.
SearchableDigraph_JML_TestData	Supply test data for the JML and JUnit based testing of SearchableDigraph.
SearchableNode	Nodes for searchable graphs.
SearchableNode_JML_TestData	Supply test data for the JML and JUnit based testing of SearchableNode.
TransposableDigraph	Transposable directed graphs.
TransposableDigraph_JML_TestData	Supply test data for the JML and JUnit based testing of TransposableDigraph.
TransposableNode	Nodes for transposable directed graphs.
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.