[<A HREF="Graph.ps">PostScript</A>]

<PRE>
Graph (N, G): <b>trait</b>
  % n1 \langle g \rangle n2 means that there is
  % an edge from n1 to n2 in g
  <b>includes</b> <A HREF="Relation.html">Relation</A> (N <b>for</b> E, G <b>for</b> R)
  <b>introduces</b>
    nodes, undirected: G -&gt; G
    isPath: N, N, G -&gt; Bool
    stronglyConnected, weaklyConnected: G -&gt; Bool
  <b>asserts</b> <b>forall</b> n1, n2: N, g: G
    undirected(g) == g \U (g\inv);
    nodes(g) == dom(g) \U range(g);
    isPath(n1, n2, g) == n1 \langle g\superstar \rangle n2;
    stronglyConnected(g) == g\superstar = nodes(g) \times nodes(g);
    weaklyConnected(g) ==
      stronglyConnected(undirected(g))
  <b>implies</b>
    <b>forall</b> n1, n2: N, g: G
      (stronglyConnected(g) /\ n1 \in nodes(g)
          /\ n2 \in nodes(g))
        =&gt; isPath(n1, n2, g)
</PRE>

[<A HREF="toc.html">Table of Contents</A>] [<A HREF="index.html">Index</A>]