// @(#)$Id: Graph.h,v 1.10 1998/09/23 02:16:43 ruby Exp $

#ifndef Graph_h
#define Graph_h

#include "Set.h"

//@ spec class Edge;

template <class Node /*@ expects contained_objects(Node) @*/ >
/*@ abstract @*/ class Graph
#include "Graph.bse"
{
public:
  //@ spec Set<Node> nodes;
  //@ spec Set<Edge> edges;
  //@ uses GraphTrait(Set<Node> for Set<N>, Node for N,
  //@                 Set<Edge> for Set<E>, Edge for E);

  virtual Graph<Node>& addNode(Node n) throw();
  //@ behavior {
  //@   modifies nodes;
  //@   ensures  nodes' = nodes^ \U {n} /\ result = self;
  //@ }

  virtual Graph<Node>& removeNode(Node n) throw();
  //@ behavior {
  //@   requires includesNode(nodes^, n) /\ isolatedNode(edges\any, n);
  //@   modifies nodes;
  //@   ensures  nodes' = nodes^ - {n} /\ result = self;
  //@ }

  virtual Node chooseNode() const throw();
  //@ behavior {
  //@   requires ~isEmpty(nodes^);
  //@   ensures  includesNode(nodes^, result);
  //@ }

  virtual Set<Node>& nodes() const throw();
  //@ behavior {
  //@   ensures fresh(result) /\ assigned(result, post)
  //@           /\ result' = nodes^;
  //@ }

  virtual int numOfNodes() const throw();
  //@ behavior {
  //@   ensures result = size(nodes^);
  //@ }

#include "Graph.pri"
};

#endif

[Index]

HTML generated using lcpp2html.