// @(#)$Id: Set.h,v 1.12 1999/04/11 15:57:37 leavens Exp $

#ifndef Set_h
#define Set_h

#include "List.h"
#include "../manual/ident_macro.lh"

template <class T /*@ expects contained_objects(T) @*/ >
  //@ where T is {
  //@   bool operator == (T x, T y);
  //@   behavior {
  //@       ensures returns /\ result = (x = y);
  //@   }
  //@ };
class Set
#include "Set.bse"
{
public:
  //@ uses SetTrait(T for E, Set<T> for C);

  Set() throw();
  //@ behavior {
  //@   modifies self;
  //@   ensures self' = {};
  //@ }

  Set(T e) throw();
  //@ behavior {
  //@   modifies self;
  //@   ensures self' = {e};
  //@ }

  ~Set() throw();
  //@ behavior {
  //@   ensures true;
  //@ }

  virtual void add(T e) throw();
  //@ behavior {
  //@   modifies self;
  //@   ensures self' = self^ \U {e};
  //@ }

  virtual void remove(T e) throw();
  //@ behavior {
  //@   modifies self;
  //@   ensures self' = delete(e, self^);
  //@ }

  virtual bool member(T e) const throw();
  //@ behavior {
  //@   ensures result = (e \in self^);
  //@ }

  virtual int size() const throw();
  //@ behavior {
  //@   ensures result = size(self\any);
  //@ }

  virtual bool isEmpty() const throw();
  //@ behavior {
  //@   ensures result = (isEmpty(self\any));
  //@ }

  virtual T ident(choose)() const throw();
  //@ behavior {
  //@   requires ~isEmpty(self\any);
  //@   ensures result = ident(choose)(self\any);
  //@ }

#include "Set.pri"
};


template <class T /*@ expects contained_objects(T) @*/ >
  //@ where T is {
  //@   bool operator == (T x, T y);
  //@   behavior {
  //@       ensures returns /\ result = (x = y);
  //@   }
  //@ };
extern bool subset(const Set<T>& s1, const Set<T>& s2) throw();
//@ behavior {
//@   uses SetTrait(T for E, Set<T> for C);
//@   requires assigned(s1, any) /\ assigned(s2, any);
//@   ensures result = (s1\any \subseteq s2\any);
//@ }

template <class T /*@ expects contained_objects(T) @*/ >
  //@ where T is {
  //@   bool operator == (T x, T y);
  //@   behavior {
  //@       ensures returns /\ result = (x = y);
  //@   }
  //@ };
extern bool operator == (const Set<T>& s1, const Set<T>& s2) throw();
//@ behavior {
//@   uses SetTrait(T for E, Set<T> for C);
//@   requires assigned(s1, any) /\ assigned(s2, any);
//@   ensures result = (s1\any = s2\any);
//@ }


template <class T /*@ expects contained_objects(T) @*/ >
  //@ where T is {
  //@   bool operator == (T x, T y);
  //@   behavior {
  //@       ensures returns /\ result = (x = y);
  //@   }
  //@ };
extern Set<T>& union_of(const Set<T>& s1, const Set<T>& s2) throw();
//@ behavior {
//@   uses SetTrait(T for E, Set<T> for C);
//@   requires assigned(s1, any) /\ assigned(s2, any);
//@   ensures fresh(result) /\ result' = (s1\any \U s2\any);
//@ }

#endif

[Index]

HTML generated using lcpp2html.