% @(#)$Id: DirectedGraphPrivateTrait.lsl,v 1.1 1997/07/25 05:32:40 leavens Exp $

DirectedGraphPrivateTrait: trait

  includes GraphTrait(Set[Node] for Set[N], Node for N,
                      Set[Edge] for Set[E], Edge for E),
           Arc_Trait, SetTrait(Arc, Set[Arc])
  assumes MutableObj(Set[Arc]), MutableObj(Node)

  introduces
    toEdges: Obj[Set[Arc]], State -> Set[Edge]
    toEdges_help: Set[Arc], State -> Set[Edge]

  asserts
    \forall osa: Obj[Set[Arc]], sa: Set[Arc], src, trgt: Obj[Node], st: State
      toEdges(osa, st) == toEdges_help(eval(osa, st), st);
      toEdges_help({}, st) == {};
      toEdges_help(insert([src, trgt], sa), st)
	 == insert(makeEdge(eval(src,st), eval(trgt,st)),
                   toEdges_help(sa, st));

  implies
    converts toEdges, toEdges_help

[Index]

HTML generated using lcpp2html.