// @(#)$Id: UndirectedGraph.h,v 1.11 1999/01/08 22:19:25 leavens Exp $

#ifndef UndirectedGraph_h
#define UndirectedGraph_h

#include "DirectedGraph.h"

template<class Node /*@ expects contained_objects(Node) @*/ >
class UndirectedGraph : public Graph<Node>
#include "UndirectedGraph.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))
  //@               => (includesEdge(edges\any, makeEdge(m,n))
  //@                   /\ includesNode(nodes\any, n)
  //@                   /\ includesNode(nodes\any, m)));

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

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

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

  virtual UndirectedGraph<Node>& removeEdge(Node n, Node m) throw();
  //@ behavior {
  //@   requires includesEdge(edges^, makeEdge(n,m));
  //@   requires redundantly includesEdge(edges^, makeEdge(m,n));
  //@   modifies edges;
  //@   ensures edges' = edges^ - ({makeEdge(n,m)} \U {makeEdge(m,n)})
  //@            /\ result = self;
  //@ }

  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\any));
  //@   ensures redundantly
  //@          includesNode(nodes^,n)
  //@           => (fresh(result) /\ assigned(result, post)
  //@               /\ \A m:Node
  //@                    ((m \in result') = (makeEdge(m,n) \in edges\any)));
  //@ }

#include "UndirectedGraph.pri"
};

#endif

[Index]

HTML generated using lcpp2html.