// @(#)$Id: IntSet2.lh,v 1.12 1997/07/31 18:19:03 leavens Exp $

#include "IntSet.lh"

//@ refine IntSet
//@ by
class IntSet {
public:
  int pick() throw();
  //@ behavior {
  //@   requires ~isEmpty(value^);
  //@   modifies value;
  //@   ensures result \in value^ /\ value' = delete(result, value^);
  //@ }

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

[Index]

HTML generated using lcpp2html.