// @(#)$Id: DirectedGraph.h,v 1.11 1999/04/11 15:57:36 leavens Exp $

#ifndef DirectedGraph_h
#define DirectedGraph_h

#include "Graph.h"

template<class Node /*@ expects contained_objects(Node) @*/ >
class DirectedGraph : public Graph<Node>
#include "DirectedGraph.bse"
{
public:
  //@ uses GraphTrait(Set<Node> for Set<N>, Node for N,
  //@                 Set<Edge> for Set<E>, Edge for E);
  //@ invariant \A n:Node, m:Node
  //@              (includesEdge(edges\any, makeEdge(n,m))
  //@               => (includesNode(nodes\any,n)
  //@                   /\ includesNode(nodes\any,m)));

  DirectedGraph() throw();  // constructor
  //@ behavior {
  //@   modifies nodes, edges;
  //@   ensures nodes' = {} /\ edges' = {};
  //@ }

  virtual ~DirectedGraph() throw();  // destructor
  //@ behavior {
  //@   ensures true;
  //@ }

  virtual DirectedGraph<Node>& addArc(Node n, Node m) throw();
  //@ behavior {
  //@   requires includesNode(nodes^,n) /\ includesNode(nodes^,m);
  //@   modifies edges;
  //@   ensures edges' = edges' \U {makeEdge(n,m)} /\ result = self;
  //@ }

  virtual DirectedGraph<Node>& removeArc(Node n, Node m) throw();
  //@ behavior {
  //@   requires includesEdge(edges^, makeEdge(n1,n2));
  //@   modifies edges;
  //@   ensures edges' = edges' - {makeEdge(n,m)} /\ result = self;
  //@ }
 
  virtual Set<Node>& adjacentNodesFrom(Node n) const throw();
  //@ behavior {
  //@   requires includesNode(nodes^,n);
  //@   ensures fresh(result) /\ assigned(result, post)
  //@           /\ \A m:Node ((m \in result')
  //@                          = (makeEdge(n,m) \in self^.arcs));
  //@ }

  virtual Set<Node>& adjacentNodesTo(Node n) const throw();
  //@ behavior {
  //@   requires includesNode(nodes^,n);
  //@   ensures fresh(result) /\ assigned(result, post)
  //@           /\ \A m:Node ((m \in result')
  //@                          = (makeEdge(m,n) \in self^.arcs));
  //@ }

  virtual Set<Node>& adjacentNodes(Node n) const throw();
  //@ behavior {
  //@   requires includesNode(nodes^,n);
  //@   ensures fresh(result) /\ assigned(result, post)
  //@           /\ \A m:Node
  //@                  ((m \in result')
  //@                   = (makeEdge(n,m) \in edges^
  //@                       \/ makeEdge(m,n) \in edges^));
  //@ }

#include "DirectedGraph.pri"
};

#endif

[Index]

HTML generated using lcpp2html.