% @(#)$Id: GraphTrait.lsl,v 1.8 1997/07/25 05:32:42 leavens Exp $

GraphTrait(N,E): trait

  includes SetTrait(N, Set[N]),
           Set(E, Set[E], int for Int)

  introduces
    includesNode: Set[N], N -> Bool
    includesEdge: Set[E], E -> Bool
    isolatedNode: Set[E], N -> Bool
    makeEdge: N, N -> E
    isEndOf: N, E -> Bool

  asserts
    E generated by makeEdge
    \forall sn: Set[N], se: Set[E], n,n1,n2: N,
            e: E, st: State
      includesNode(sn, n) == n \in sn;
      includesEdge(se, e) == e \in se;
      isolatedNode({}, n);
      isolatedNode(insert(e,se), n)
        == ~isEndOf(n,e) /\ isolatedNode(se,n);
      isEndOf(n, makeEdge(n1,n2)) == (n = n1 \/ n = n2);

  implies
    converts includesNode, includesEdge, isolatedNode, isEndOf

[Index]

HTML generated using lcpp2html.