// @(#)$Id: List.h,v 1.13 1999/04/11 15:57:37 leavens Exp $
// Lists as in LISP, based on William Cook's paper:
// Object-Oriented Programming Versus Abstract Data Types,
// Foundations of Object-Oriented Languages, REX School/Workshop,
// Noordwijkerhout, The Netherlands, May/June 1990, Springer-Verlag,
// LNCS 489, 1991.

#ifndef List_h
#define List_h

#include "pretend_bool.h"

template <class T /*@ expects contained_objects(T) @*/>
/*@ abstract @*/ class List
#include "List.bse"
{
public:
  //@ uses ListTrait(T for E, List<T> for C);

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

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

  virtual List<T>* 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);
  //@ }

#include "List.pri"
};

template <class T /*@ expects contained_objects(T) @*/ >
class Nil : public List<T>
#include "Nil.bse"
{
public:
  //@ uses NilTrait(T for E, List<T> for C, Nil<T> for EmptyList);
  //@ simulates List<T> by toList;

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

  // The following are implemented,  but to the same specs as above.
  bool is_null() const throw();
  T head() const throw();
  List<T>* tail() const throw();

#include "Nil.pri"
};


// Common code for ImmutableList and Cons (mutable lists).

template <class T /*@ expects contained_objects(T) @*/ >
/*@ abstract @*/ class NonEmptyList : public List<T>
#include "NonEmptyList.bse"
{
public:
  //@ uses NonEmptyListTrait(T for E, List<T> for C,
  //@                        NonEmptyList<T> for NEList);
  //@ simulates List<T> by toList;
  //@ invariant len(self\any) >= 1;

  // The following are implemented,  but to the same specs as above.
  bool is_null() const throw();
  T head() const throw();
  List<T>* tail() const throw();

#include "NonEmptyList.pri"
};


// Lists that cannot be mutated.
// The assurance of no mutation comes fom the type restrictions
// on the constructors.

template <class T /*@ expects contained_objects(T) @*/ >
class ImmutableList : public NonEmptyList<T>
#include "ImmutableList.bse"
{
public:
  //@ uses ImmutableListTrait(T for E, List<T> for C,
  //@                         NonEmptyList<T> for NEList,
  //@                         ImmutableList<T> for IMList);
  //@ simulates NonEmptyList<T> by toNEList;
  //@ constraint self^ = self';

  ImmutableList(T x, ImmutableList<T>* l) throw();
  //@ behavior {
  //@    requires assigned(l, pre);
  //@    modifies self;
  //@    ensures self' = {x} || (*l)\pre;
  //@ }

  ImmutableList(T x, Nil<T>* l) throw();
  //@ behavior {
  //@    requires allocated(l, pre);
  //@    modifies self;
  //@    ensures self' = {x};
  //@ }

#include "ImmutableList.pri"
};

#endif

[Index]

HTML generated using lcpp2html.