// @(#)$Id: intlist.h,v 1.7 1997/07/28 21:38:13 leavens Exp $

#ifndef intlist_h
#define intlist_h

class listelem
#include "intlist.bse"
{
private:
  int car;
  listelem * cdr;
  //@ invariant isLegal(cdr\any);   // see the Larch/C++ Pointer trait

public:

  listelem(int val = 0, listelem * next = 0) throw();
  //@ behavior {
  //@   modifies car, cdr;
  //@   ensures car' = val /\ cdr' = next;
  //@ }

  int get_value() const throw();
  //@ behavior {
  //@   ensures result = car\any;
  //@ }

  listelem * get_next() const throw();
  //@ behavior {
  //@   ensures result = cdr\any;
  //@ }

  void set_value(int i) throw();
  //@ behavior {
  //@   ensures car' = i;
  //@ }

  void set_next(listelem * l) throw();
  //@ behavior {
  //@   ensures cdr' = l;
  //@ }
};

// auxiliary functions

typedef listelem * list;   // implicitly uses Pointer(Obj, listelem);

extern list  empty() throw();
//@ behavior {
//@   ensures result = 0;
//@ }

extern bool  isempty( list l ) throw();
//@ behavior {
//@   requires isLegal(l);
//@   ensures result = (isNull(l));
//@ }
  
extern bool  equal( list l1, list l2 ) throw();
//@ behavior {          // This is equality of values, not LISP's eq.
//@   uses ToListTrait;
//@   requires not(circular(l1, pre) \/ circular(l2, pre));
//@   ensures result = (toList(l1,pre) = toList(l2,pre));
//@ }

extern int   top( list l ) throw();
//@ behavior {
//@   requires assigned(l, pre);  // which implies that l is not NULL
//@   ensures result = (*l)^.car^;
//@ }

extern list  rest( list l ) throw();
//@ behavior {
//@   requires assigned(l, pre);
//@   ensures result = (*l)^.cdr^;
//@ }

extern list  append( int i, list l ) throw();
//@ behavior { 
//@   requires isLegal(l);
//@   ensures fresh(result) /\ isValid(result)
//@           /\ (*result)'.car' = i /\ (*result)'.cdr' = l;
//@ }

extern list  copy( list l ) throw();
//@ behavior {
//@   uses ToListTrait;
//@   requires isLegal(l) /\ not(circular(l, pre));
//@   ensures fresh(list_objs(result, post))
//@           /\ toList(l,pre) = toList(result,post);
//@ }

// Note that the function conc which follows can make a circular list.
// If you don't want to make a circular list,
// be sure that l2 is not top-level aliased with any part of l1.
// In Larch/C++ such an assertion can be written if one
//	uses ToListTrait;
// as follows
//	not(top_level_aliased(l1, l2, pre))
// This assertion could be included in the precondition if desired.

extern list  conc( list l1, list l2 ) throw();
//@ behavior { 
//@   uses ToListTrait;
//@
//@   requires isNull(l1);
//@   ensures result = l2;
//@ also
//@   requires isValid(l1) /\ not(circular(l1, pre));
//@   modifies last_elem(l1, pre);
//@   ensures result = l1 /\ last_elem(l1, post)'.cdr' = l2;
//@ }

#endif

[Index]

HTML generated using lcpp2html.