// @(#)$Id: PriorityQueue.lh,v 1.13 1998/09/23 16:02:04 ruby Exp $

template <class Elem /*@ expects PriorityQueueRequirement(Elem) @*/>

  //@ where Elem is {
  //@   bool operator <= (Elem x, Elem y);
  //@   behavior {
  //@     ensures returns /\ result = (x <= y);
  //@   }
  //@ };

class PriorityQueue {
public:
  //@ uses PriorityQueueTrait(PriorityQueue<Elem> for PQ[Elem]);

  PriorityQueue() throw();
  //@ behavior {
  //@   modifies self;
  //@   ensures liberally self' = empty;
  //@ }

  PriorityQueue(const PriorityQueue<Elem>& oth) throw();
  //@ behavior {
  //@   modifies self;
  //@   ensures liberally self' = oth\any;
  //@ }

  virtual ~PriorityQueue() throw();
  //@ behavior {
  //@   trashes self;
  //@   ensures allocated(self, post);
  //@   ensures redundantly assigned(self, post) => unchanged(self);
  //@   example unchanged(self);
  //@   example ~assigned(self,post);
  //@ }

  virtual void Insert(Elem e) throw();
  //@ behavior {
  //@   modifies self;
  //@   ensures liberally self' = add(e, self^);
  //@ }

  virtual Elem Largest() const throw();
  //@ behavior {
  //@   requires len(self^) >= 1;
  //@   ensures result = head(self^);
  //@ }

  virtual Elem RemoveLargest() throw();
  //@ behavior {
  //@   requires len(self^) >= 1;
  //@   modifies self;
  //@   ensures result = head(self^) /\ self' = tail(self^);
  //@ }

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

  virtual long int Length() const throw();
  //@ behavior {
  //@   ensures liberally result = len(self\any);
  //@ }

  virtual long int Count(Elem e) const throw();
  //@ behavior {
  //@   ensures liberally result = count(self\any);
  //@ }
};

[Index]

HTML generated using lcpp2html.