/*
// AlgoDat SS00, Aufgabe 45
// Christian Semrau, 08.05.2000

Type Sequenz[X]

Functions:
  mt_sequenz: --> Sequenz[X]                    Konstruktor

  insert_begin: Sequenz[X] x X -/-> Sequenz[X]  Konstruktor
  insert_end: Sequenz[X] x X -/-> Sequenz[X]    Konstruktor
  // das "Abweisen" von doppelten Eintraegen erfolgt durch Preconditions

  del: Sequenz[X] x INT -/-> Sequenz[X]         Selektor
  search: Sequenz[X] x INT -/-> X               Selektor
  // realisiert eigentlich eine "elementAt"-Funktion
  // Indizes beginnen bei 0

  empty: Sequenz[X] --> BOOL                    Praedikat
  size: Sequenz[X] --> INT
  min: Sequenz[X] -/-> X                        Selektor
  max: Sequenz[X] -/-> X                        Selektor
  clear: Sequenz[X] --> Sequenz[X]

  // Hilfsfunktionen
  min: X x X --> X
  max: X x X --> X

Axioms: forall S: Sequenz[X], x, y: X, n: INT
  // die Datentypen der Variablen muessen angegeben werden

  // die beiden Axiome setzen alle Sequenzen gleich, die die gleichen
  // Elemente in der gleichen Reihenfolge haben, unabhaengig von der
  // Reihenfolge der insert_begin und insert_end, deshalb genuegt es,
  // die anderen Funktionen nur fuer insert_end zu betrachten
  insert_begin(mt_sequenz, x) = insert_end(mt_sequenz, x)
  insert_begin(insert_end(S, y), x) = insert_end(insert_begin(S, x), y)

  del(insert_end(S, x), n) = if n=size(S) then S else insert_end(del(S, n), x)
  search(insert_end(S, x), n) = if n=size(S) then x else search(S, n)

  empty(S) <-> size(S) = 0
  size(mt_sequenz) = 0
  size(insert_end(S, x)) = size(S) + 1

  min(insert_end(mt_sequenz, x)) = max(insert_end(mt_sequenz, x)) = x
  min(insert_end(S, x)) = min(min(S), x)
  max(insert_end(S, x)) = max(max(S), x)

  clear(S) = mt_sequenz

  // Hilfsfunktionen
  min(x, y) = if x<y then x else y
  max(x, y) = if x<y then y else x

  // die Umkehrung von search: search(S,n)=x <-> search2(S,x)=n
  // gehoert nicht zum ADT, wuerde aber die Preconditions von
  // insert_begin und insert_end vereinfachen
//  search2(mt_sequenz, x) = -1
//  search2(insert_end(S, x), y) = if x=y then size(S) else search2(S, y)

Preconditions: forall S: Sequenz[X], x: X, n: INT
  pre(del   (S, n)): n>=0 AND n<size(S)  // das impliziert size(S)>0
  pre(search(S, n)): n>=0 AND n<size(S)
  pre(min(S)): size(S)>0
  pre(max(S)): size(S)>0
  pre(insert_begin(S, x)): forall m el {0, size(S)-1}: search(S, m) != x
  pre(insert_end  (S, x)): forall m el {0, size(S)-1}: search(S, m) != x
*/

/**
 * AlgoDat SS00, Aufgabe 45
 * ADT Sequenz, Testklasse
 * 
 * @author Christian Semrau
 * <a href="mailto:gsemrau@cs.uni-magdeburg.de">gsemrau@cs.uni-magdeburg.de</a>
 */
class SequenzTest{

public static void main(String[] args){

  // leere Sequenz erzeugen
  Sequenz S = Sequenz.mt_sequenz();
  System.out.println("S = "+S+", size = "+Sequenz.size(S)+", empty = "+Sequenz.empty(S));

  // anfuegen am Anfang und am Ende
  Sequenz.insert_end(Sequenz.insert_begin(S, new X(100)), new X(101));
  System.out.println("S = "+S+", size = "+Sequenz.size(S)+", empty = "+Sequenz.empty(S));

  // ein Element holen
  System.out.println("search(S, 1) = "+Sequenz.search(S, 1));
  Sequenz.insert_begin(S, new X(102));
  System.out.println("S = "+S+", size = "+Sequenz.size(S)+", empty = "+Sequenz.empty(S));

  // Maximum und Minimum
  System.out.println("max(S) = "+Sequenz.max(S)+", min(S) = "+Sequenz.min(S));

  // del und size
  Sequenz.del(S, Sequenz.size(S)-1);
  System.out.println("S = "+S+", size = "+Sequenz.size(S)+", empty = "+Sequenz.empty(S));

  // insert_end mit Exception
  try{
    Sequenz.insert_end(S, Sequenz.search(S, 0));
  }catch(IllegalArgumentException exc){
    System.out.println(exc);
  }

  // wiederholtes Einfuegen am Anfang
  for(int i=10; i>=0; i--)
    Sequenz.insert_begin(S, new X(i));
  System.out.println("S = "+S+", size = "+Sequenz.size(S)+", empty = "+Sequenz.empty(S));

  // del und size
  Sequenz.del(S, S.size(S)-2);
  Sequenz.del(S, 0);
  Sequenz.del(S, Sequenz.size(S)-1);
  System.out.println("S = "+S+", size = "+Sequenz.size(S)+", empty = "+Sequenz.empty(S));

  // wiederholtes Einfuegen am Ende
  for(int i=11; i<15; i++)
    Sequenz.insert_end(S, new X(i));
  System.out.println("S = "+S+", size = "+Sequenz.size(S)+", empty = "+Sequenz.empty(S));

  // Sequenz leeren
  Sequenz.clear(S);
  System.out.println("S = "+S+", size = "+Sequenz.size(S)+", empty = "+Sequenz.empty(S));
}
} // SequenzTest

/**
 * AlgoDat SS00, Aufgabe 45
 * Implementierung der Sequenz mit einem Array
 */
class Sequenz{

// Methoden des abstrakten Datentyps
  
/** Legt eine neue Sequenz an */
public static Sequenz mt_sequenz() {
  return new Sequenz();
}

/** Leert die Sequenz */  
public static Sequenz clear(Sequenz S){
  return S.clear();
}

/** Entfernt ein Element aus der Sequenz */
public static Sequenz del(Sequenz S, int I){
  return S.del(I);
}

/** true, wenn die Sequenz leer ist */
public static boolean empty(Sequenz S){
  return S.empty();
}

/** Fuegt ein Element am Anfang ein */
public static Sequenz insert_begin(Sequenz S, X x){
  return S.insert_begin(x);
}

/** Fuegt ein Element am Ende ein */
public static Sequenz insert_end(Sequenz S, X x){
  return S.insert_end(x);
}

/** Liefert das Maximum der Sequenz */
public static X max(Sequenz S){
  return S.max();
}

/** Liefert das Minimum der Sequenz */
public static X min(Sequenz S){
  return S.min();
}

/** Liefert das Element am gegebenen Index */
public static X search(Sequenz S, int I){
  return S.search(I);
}

/** Liefert die Laenge der Sequenz */
public static int size(Sequenz S){
  return S.size();
}

// Objektorientierte Implementierung

public Sequenz() {
  loadstep=10; feld=new X[2*loadstep]; offset=loadstep; length=0;
  min = max = null;
}

public Sequenz clear(){
  offset = feld.length/2; length = 0;
  for (int i=0; i<feld.length; )
    feld[i++] = null;  // gibt die Objekte frei fuer den GC
  min = max = null;
  return this;
}

public Sequenz del(int I){
  if (I<0 || I>=length)
    throw new IllegalArgumentException(I+" ausserhalb der Sequenz");
  min = max = null;
  // wir machen uns nicht die Muehe, das neue min und max zu bestimmen  

  if (I==0){ feld[offset++] = null; length--;
  }else
  if (I==length-1){ feld[offset+(--length)] = null;
  }else{
    System.arraycopy(feld,offset+I+1, feld,offset+I, length-I-1);
    feld[offset+(--length)] = null;
  }
  return this;
}

public boolean empty(){
  return length == 0;
}

public Sequenz insert_begin(X x){
  if (x == null) throw new NullPointerException("Darf null nicht speichern");
  if (search2(x)>=0) throw new IllegalArgumentException(x+" schon vorhanden");
  if (offset<=0) resize();

  // max anpassen
  if (max != null)  // Maximum existiert
    max = max.max(x);  // sieht lustig aus, tut aber was es soll:
    // liefert das neue Maximum
  else
  if (length == 0)  // wenn die Sequenz vorher leer war, gilt das neue...
  // Element als Minimum und Maximum
    min = max = x;
  // sonst bleibt max==null

  feld[--offset] = x; length++;
  return this;
}

public Sequenz insert_end(X x){
  if (x == null) throw new NullPointerException("Darf null nicht speichern");
  if (search2(x)>=0) throw new IllegalArgumentException(x+" schon vorhanden");
  if (offset+length>=feld.length) resize();
  if (min != null) min = min.min(x); else if (length==0) min = max = x;
  feld[offset+(length++)] = x;
  return this;
}

public X max() {
  if (length<=0) throw new IllegalArgumentException("max von leerer Sequenz");
  if (max != null) return max; // wenn max existiert, einfach zurueckgeben
  X m = feld[offset];
  for (int i=offset+1; i<offset+length; m = m.max(feld[i++]));
  return max = m; // neues max gefunden
}

public X min() {
  if (length<=0) throw new IllegalArgumentException("min von leerer Sequenz");
  if (min != null) return min; // wenn min existiert, einfach zurueckgeben
  X m = feld[offset];
  for (int i=offset+1; i<offset+length; m = m.min(feld[i++]));
  return min = m; // neues min gefunden
}

public X search(int I){
  if (I<0 || I>=length)
    throw new IllegalArgumentException(I+" ausserhalb der Sequenz");
  return feld[offset+I];
}

public int size(){
  return length;
}

// interne Variablen der Sequenz

  private X[] feld;  // Feld, das die Daten enthaelt
  private int offset;  // Beginn des Datenbereichs
  private int length;  // Laenge des Datenbereichs
  private int loadstep;  // gibt den gewuenschten Platz am Anfang...
  // und Ende des Feldes beim Vergroessern an
  private X min, max; // aktuelles Minimum und Maximum

// interne Hilfsmethoden

private void resize() {
    int l = loadstep>0 ? loadstep : (length+2);
    X[] feld2 = new X[length+2*l];
    System.arraycopy(feld,offset, feld2,l, length);
    feld = feld2; offset=l;
}

private int search2(X x){
  for (int i=offset; i<offset+length; i++)
    if (x.equals(feld[i])) return i-offset;
  return -1;
}

// fuer Ausgabe der Sequenz

public String toString() {
  StringBuffer sb = new StringBuffer();
  sb.append("{");
  if (length>0) sb.append(feld[offset]);
  for (int i=offset+1; i<offset+length; i++)
    sb.append(",").append(feld[i]);
//  sb.append("}-(").append(offset+","+length+","+feld.length);
  sb.append(")");
  return sb.toString();
}
} // Sequenz

/** Elemente der Sequenz */
class X{
  private int value; // Interne Daten
  public X(int v) { value = v; } // Konstruktor

  // Vergleichsmethoden
  boolean equals(X j) { return value==j.value; }
  boolean kleiner(X j) { return value<j.value; }
  X max(X j) { if (value<j.value) return j; else return this; }
  X min(X j) { if (value<j.value) return this; else return j; }
  public String toString() { return ""+value; }
} // X