// @(#)$Id: Graph.pri,v 1.4 1999/04/11 15:57:36 leavens Exp $
// private and protected members for Graph

protected:
  Set<Node> the_nodes;
  //@ depends nodes on the_nodes;
  //@ invariant nodes\any = the_nodes\any;

  Graph<Node>(Set<Node> ns)
  //@ behavior {
  //@   modifies nodes;
  //@   modifies redundantly the_nodes;
  //@   ensures nodes' = ns;
  //@   ensures redundantly the_nodes' = ns;
  //@ }
    : the_nodes(ns)
{
}