// @(#)$Id: IntList.lh,v 1.13 1997/06/03 20:29:38 leavens Exp $

//@ uses List(int for E, IntList for C), NoContainedObjects(IntList);

/*@ abstract @*/ class IntList {
public:
  virtual bool is_null() const throw() = 0;
  //@ behavior {
  //@   ensures result = (self\any = empty);
  //@ }

  virtual int head() const throw() = 0;
  //@ behavior {
  //@   requires ~(self\any = empty);
  //@   ensures result = head(self\any);
  //@ }

  virtual IntList* tail() const throw() = 0;
  //@ behavior {
  //@   requires ~(self\any = empty);
  //@   ensures isValid(result) /\ (*result)' = tail(self\any);
  //@ }

  virtual int length() const throw();
  //@ behavior {
  //@   requires len(self\any) <= INT_MAX;
  //@   ensures result = len(self\any);
  //@ }
};

[Index]

HTML generated using lcpp2html.