Graph (N, G): trait
  % n1 \langle g \rangle n2 means that there is
  % an edge from n1 to n2 in g
  includes Relation (N for E, G for R)
    nodes, undirected: G -> G
    isPath: N, N, G -> Bool
    stronglyConnected, weaklyConnected: G -> Bool
  asserts forall 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) ==
    forall n1, n2: N, g: G
      (stronglyConnected(g) /\ n1 \in nodes(g)
          /\ n2 \in nodes(g))
        => isPath(n1, n2, g)
[Table of Contents] [Index]