// name_list9.cc 
//
//  mit Frameregeln, Implementierung mit Iterator
//                   und Nutzung des Iterators in der Methode
//                   display_contents() und in main() sowie
//                   den Frame-Regeln, Qstl-Quantoren
// (Problem die Qstl-Quantoren arbeiten "nur" mit iterator,
//  nicht mit const_iterator)
//
// Entfernung der Dxxx()-Makros
//
// Contracts für den Iterator, funktionale Schreibweise der Nachbedingung

#define EIFFEL_DOEND

// NANA ganz ausschalten:
// #define WITHOUT_NANA

#include <eiffel.h>
#include "nana.h"
#include <Qstl.h>

#include <iostream>
#include <vector>
#include <set>

// Erzeuge Produktionsversion:
//#define EIFFEL_CHECK  CHECK_REQUIRE
// eventuell: (dann aber die ID()-definierten Variablen nicht als
//                                  guards bneutzen, da ...
//#define ID(e) /* empty */
//#define IS(e) /* empty */

// Erzeuge Entwicklungsversion:
#define EIFFEL_CHECK  CHECK_ALL

using namespace std;

///////////////// Hilfsfunktionen //////////////////////////

template <class T>
set<T> operator+(const set<T>& s, const T& e){
    set<T> result(s);
    result.insert(e);
    return result;
};

template <class T>
set<T> operator-(const set<T>& s, const T& e){
    set<T> result(s);
    result.erase(e);
    return result;
};

///////////////// class declaration ////////////////////////

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::const_iterator /////////

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; 
};

///////////////// name_list class definition /////////////

unsigned int name_list::position_of(const string& a_name) const{

    unsigned int index(1);
    unsigned int result;
    for(; (index<=count) && (the_contents->at(index-1)!=a_name); index++);
    if (index <= count)
	result = index;
    else
        result = 0;    

    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))));
    return result;
};

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

unsigned int name_list::get_count() const{    // number of items in stack

    unsigned int result = count;
    ENSURE(result == count);
    return result;
};

bool name_list::has(const string& a_name) const{

    bool result = (position_of(a_name) > 0);
    ENSURE((get_count()>0) || !result);
    ENSURE(result == EO(i, (*this), (*i)==a_name));
    return result;
};

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

bool name_list::invariant() const{
    return (count >= 0) && (the_contents != 0);
};    

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

void name_list::display_contents() const{     // print contents of list to cout

    cout << endl << "Anzahl der Listenelemente: " << count << endl;
    for (name_list::iterator i = begin(); i != end(); i++)
	cout << "  " << *i;
    cout << endl << endl;
    // ENSURE('Drucke alle Namen in Name_list');
};

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

name_list::name_list(): count(0), the_contents(new vector<string>(100)){
    CHECK(invariant());
};

name_list::~name_list(){                  // notwendig wegen new in Konstruktor
    REQUIRE(the_contents != 0);
    delete the_contents;
};

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

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));
   
   count++;
   the_contents->at(count-1) = 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));

   the_contents->at(position_of(a_name)-1) = the_contents->at(count-1);
   count--;

   ENSURE(! has(a_name));
   ENSURE((!pre) || (get_count() == count_old -1));
   // Menge der Einträge in list == Menge der Einträge in list_old ohne a_name
   ID(set<string> contents(begin(),end()));
   ENSURE((!pre) || (contents == contents_old - a_name));
END;

//////////////// child class relaxed_name_list ///////////
////////////////   (more user friendly)   ////////////////

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
 
};

///////// invariant:

bool relaxed_name_list::invariant() const{

    return name_list::invariant(); // && weitere einschränkende Bedingungen
    // return name_list::invariant() && (count<=2); // Test

};

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

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));
   
   if (!has(a_name)) {
      count++;
      the_contents->at(count-1) = a_name;
   };

   ENSURE(has(a_name));
   ENSURE((!not_in_list) || (get_count() == count_old + 1));  // &&
   ENSURE(  not_in_list  || (get_count() == count_old));
   // Für alle s in list_old: has(s)
   // Für alle s in list:     (s == a_name) || s in list_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));

   if (has(a_name)){
      the_contents->at(position_of(a_name)-1) = the_contents->at(count-1);
      count--;
   };

   ENSURE(!has(a_name));
   ENSURE((!pre_parent) || (get_count() == count_old -1));  // &&
   ENSURE(  pre_parent  || (get_count() == count_old));
   // Menge der Einträge in list == Menge der Einträge in list_old ohne a_name
   ID(set<string> contents(begin(),end()));
   ENSURE(  pre_parent  || (contents == contents_old));;
   ENSURE((!pre_parent) || (contents == contents_old - a_name));
END;

/// contract for Iterator:  (as a basic query)
//
//        Überlege weitere Vor- und Nachbedingungen
//

name_list::iterator::iterator(const name_list* const init){

    name_list_base_ptr = init;
    if ((name_list_base_ptr != 0)&&(name_list_base_ptr->count > 0)){
	index = 0;
    } else
        index = -1;
    if (index == -1) name_list_base_ptr = 0;
    // (*this)=="first" element of name_list (*init) if (init != 0),
    // this is an unique iterator not in any name_list if (init == 0)
};

name_list::iterator name_list::begin() const {
    iterator result = iterator(this);
    // returns iterator pointing to "first" element of name_list
    // or same as end(), when name_list is empty
    ENSURE((count < 1 ) || (result != end()));
    ENSURE((count >= 1) || (result == end()));
    return result;
};


name_list::iterator name_list::end() const {
    return iterator();
    // returns iterator denoting to be not any more in name_list,
    // an unique iterator not in any name_list
};

string name_list::iterator::operator*() const {
    REQUIRE((name_list_base_ptr!=0) && ((*this)!=name_list_base_ptr->end()));
    return name_list_base_ptr->the_contents->at(index);
    // return element, iterator is pointing to;
    // name_list of iterators not changed
};

name_list::iterator& name_list::iterator::operator++(){ // Präfix
    if (name_list_base_ptr != 0){
	index++;
        if (index > name_list_base_ptr->count-1){
	    index = -1;
	    name_list_base_ptr = 0;
        };
    };
    return *this;
    // increment position of iterator and return reference to this
    //       incremented iterator afterwards,
    // name_list not changed
};

name_list::iterator  name_list::iterator::operator++(int){//Postfix
    iterator temp = *this;
    ++*this;
    return temp;
    // return copy of iterator and as a side effect increment position
    //      of the actual iterator,
    // name_list not changed
};

bool name_list::iterator::operator==(const name_list::iterator& x) const{
    return ((name_list_base_ptr == x.name_list_base_ptr)&&(index == x.index));
   // return if iterator and x point to the same element in the
   // same name_list
};

bool name_list::iterator::operator!=(const name_list::iterator& x) const{
    return !(*this == x);
    // ENSURE(!((*this)==x));          // Konsistenzbedingung
};

//////////////// class test main() program ///////////////

int main(){

    cout << "\nTest der Klasse name_list: ----------------" << endl;

    { name_list s;
    s.display_contents();

    s.put("Richard"); s.display_contents();
    // s.put("Richard"); s.display_contents(); // Test für pre-Verletzung 
    s.put("Helen"); s.display_contents();
    s.put("Yu"); s.display_contents();
    s.put("Jim"); s.display_contents();
    s.put("Chen"); s.display_contents();
    s.put("Moira"); s.display_contents();
    s.put("Jens"); s.display_contents();

    s.remove("Chen"); s.display_contents();
    // s.remove("Chen"); s.display_contents();
    s.remove("Richard"); s.display_contents();
    s.remove("Yu"); s.display_contents();
    s.remove("Moira"); s.display_contents();
    s.remove("Helen"); s.display_contents();
    s.remove("Jens"); s.display_contents();
    s.remove("Jim"); s.display_contents();
    // s.remove("Karl"); s.display_contents();

    };

    cout << "\nTest der Kindklasse relaxed_name_list: ----" << endl;

    { relaxed_name_list s;
    s.display_contents();

    // relaxed_name_list s2(s);

    s.put("Richard"); s.display_contents();
    s.put("Richard"); s.display_contents(); // Test für pre-Verletzung 
    s.put("Helen"); s.display_contents();
    s.put("Yu"); s.display_contents();
    s.put("Jim"); s.display_contents();
    s.put("Chen"); s.display_contents();
    s.put("Moira"); s.display_contents();
    s.put("Jens"); s.display_contents();

    cout << "Benutzung des iterators:\n";
    for(name_list::iterator it = s.begin(); it != s.end(); it++)
	cout << *it << " --- ";
    cout << endl;

    s.remove("Chen"); s.display_contents();
    s.remove("Chen"); s.display_contents();
    s.remove("Richard"); s.display_contents();
    s.remove("Yu"); s.display_contents();
    cout << "Benutzung des iterators:\n";
    for(name_list::iterator it = s.begin(); it != s.end(); it++)
	cout << *it << " --- ";
    cout << endl;
    s.remove("Moira"); s.display_contents();
    s.remove("Helen"); s.display_contents();
    s.remove("Jens"); s.display_contents();
    s.remove("Jim"); s.display_contents();
    s.remove("Karl"); s.display_contents();

    };

    cout << "\nTestende ------------------" << endl << endl;

}