...
#define EIFFEL_DOEND
...
#include <eiffel.h>
#include "nana.h"
#include <Qstl.h>
#include <iostream>
#include <vector>
#include <set>
...
#define EIFFEL_CHECK  CHECK_ALL
...
template <class T>
set<T> operator+(const set<T>& s, const T& e){
    ...
};
...
template <class T>
set<T> operator-(const set<T>& s, const T& e){
    ...
};
...
class name_list{

protected:

  vector<string>* the_contents;
  unsigned int count;

  // private support function

  unsigned int position_of(const string& a_name) const;

public:

  /////////// basic queries: 

  unsigned int get_count() const;        // number of items in stack

  bool has(const string& a_name) const;

  /////////// Iteratoren:

  class iterator;
  friend class iterator;

  iterator begin() const;
  iterator end() const;

  /////////// class invariant:

protected:
  virtual bool invariant() const;    
public:

  /////////// derived queries:

  void display_contents() const;         // print contents of list to cout

  /////////// constructors:

  name_list();

  virtual ~name_list();              // notwendig wegen new in Konstruktor

private:                             // disable default methods

  name_list(const name_list& s);
  name_list& operator=(const name_list& s);
  
public:

/////////// (pure) modificators:

  virtual void put(const string& a_name);       // Push a_name into list

  virtual void remove(const string& a_name);    // delete a_name in list
 
};
...
class name_list::iterator{

    int index;
    const name_list* name_list_base_ptr;

    // Überlege sinnvolle Invariante!

public:

    iterator(const name_list* const init = 0);

    string operator*() const;        // Zugriff auf Elemet am Iterator-Ort
    iterator& operator++();    // Präfix-Inkrement
    iterator  operator++(int); // Postfix-Inkrement
  
    bool operator==(const iterator& x) const; // Vergleich von Iteratoren
    bool operator!=(const iterator& x) const; 
};
...
unsigned int name_list::position_of(const string& a_name) const{
    ...
    ID(iterator i = begin());
    IS(for(int z=1; z<result; i++,z++));
    ENSURE(/* a_name in list */ 
                                ((1<=result)&&(result<=get_count())&&
                                                          ((*i)==a_name))||
       	   /* otherwise: */
                              ((0 == result)&&(!EO(j,(*this),(*j)==a_name))));
    ...
};
...
unsigned int name_list::get_count() const{    // number of items in stack
    ...
    ENSURE(result == count);
    ...
};
bool name_list::has(const string& a_name) const{
    ...
    ENSURE((get_count()>0) || !result);
    ENSURE(result == EO(i, (*this), (*i)==a_name));
    ...
};
...
bool name_list::invariant() const{
    ...
};    
...
void name_list::display_contents() const{     // print contents of list to cout
    ...
};
...
name_list::name_list(): count(0), the_contents(new vector<string>(100)){
    ...
};
name_list::~name_list(){                  // notwendig wegen new in Konstruktor
    REQUIRE(the_contents != 0);
    ...
};
...
void name_list::put(const string& a_name)    // Push a_name into list
DO
   REQUIRE(/* name not in list */    !has(a_name));
   ID(set<string> contents_old(begin(),end()));
   ID(int count_old = get_count());
   ID(bool not_in_list = !has(a_name));
   ...
   ENSURE(has(a_name));
   ENSURE( (!not_in_list) || (get_count() == count_old + 1));
   ID(set<string> contents(begin(),end()));
   ENSURE( (!not_in_list) || (contents == contents_old + a_name));
END;
void name_list::remove(const string& a_name) // delete a_name in list
DO
   REQUIRE(/* name in list */     has(a_name));
   ID(set<string> contents_old(begin(),end()));
   ID(int count_old = get_count());
   ID(bool pre = has(a_name));
   ...
   ENSURE(! has(a_name));
   ENSURE((!pre) || (get_count() == count_old -1));
   ...
   ID(set<string> contents(begin(),end()));
   ENSURE((!pre) || (contents == contents_old - a_name));
END;
...
class relaxed_name_list : public name_list{

public:

    ///////// invariant:

    virtual bool invariant() const;

    ///////// (pure) modificators: (redefined)

    virtual void put(const string& a_name);       // Push a_name into list

    virtual void remove(const string& a_name);    // delete a_name in list
 
};
...
bool relaxed_name_list::invariant() const{
    ...
};
...
void relaxed_name_list::put(const string& a_name)    // Push a_name into list
DO 
   REQUIRE(/* nothing */  true);       // pre_parent || has(a_name)
   ID(set<string> contents_old(begin(),end()));
   ID(int count_old = get_count());
   ID(bool not_in_list = !has(a_name));
   ...
   ENSURE(has(a_name));
   ENSURE((!not_in_list) || (get_count() == count_old + 1));  // &&
   ENSURE(  not_in_list  || (get_count() == count_old));
   ...
   ID(set<string> contents(begin(),end()));
   ENSURE(  not_in_list  || (contents == contents_old));
   ENSURE((!not_in_list) || (contents == contents_old + a_name));
END;
void relaxed_name_list::remove(const string& a_name) // delete a_name in list
DO
   REQUIRE(/* nothing */ true);        // pre_parent || !has(a_name)
   ID(set<string> contents_old(begin(),end()));
   ID(int count_old = get_count());
   ID(bool pre_parent = has(a_name));
   ...
   ENSURE(!has(a_name));
   ENSURE((!pre_parent) || (get_count() == count_old -1));  // &&
   ENSURE(  pre_parent  || (get_count() == count_old));
   ...
   ID(set<string> contents(begin(),end()));
   ENSURE(  pre_parent  || (contents == contents_old));;
   ENSURE((!pre_parent) || (contents == contents_old - a_name));
END;
...
name_list::iterator::iterator(const name_list* const init){
    ...
};
name_list::iterator name_list::begin() const {
    ...
    ENSURE((count < 1 ) || (result != end()));
    ENSURE((count >= 1) || (result == end()));
    ...
};
name_list::iterator name_list::end() const {
    ...
};
string name_list::iterator::operator*() const {
    REQUIRE((name_list_base_ptr!=0) && ((*this)!=name_list_base_ptr->end()));
    ...
};
name_list::iterator& name_list::iterator::operator++(){ // Präfix
    ...
};
name_list::iterator  name_list::iterator::operator++(int){//Postfix
    ...
};
bool name_list::iterator::operator==(const name_list::iterator& x) const{
    ...
};
bool name_list::iterator::operator!=(const name_list::iterator& x) const{
    ...
};
...
int main(){
    ...
}