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.