// Christian Semrau

Type: STRING

Functions:
  mt_string: STRING                    Konstruktor
  cons: STRING x CHAR --> STRING       Konstruktor
  last: STRING -/-> CHAR               Selektor
  is_mt: STRING --> BOOL               Praedikat
  is_equal: STRING x STRING --> BOOL   Praedikat
  length: STRING --> INT
  number_of: STRING x CHAR --> INT
  concat: STRING x STRING --> STRING

Axioms: forall s,t,u: STRING, c,d: CHAR
  length(mt_string) = zero
  length(cons(s, c)) = succ(length(s))
// die Laenge des Strings wird durch fortgesetzte Abspaltung des letzten Zeichens ermittelt.

  is_mt(s) <-> is_equal(s, mt_string)
 <-> is_equal(mt_string, s) <-> (length(s) = 0)
// Axiome die feststellen, ob ein String leer ist

  is_equal(cons(s, c), cons(t, d)) <-> ((c = d) AND is_equal(s, t))
// is_equal wird definiert durch Vergleich der einzelnen Zeichen,
 beginnend beim letzten.
// So kommen wir irgendwann zu einem Parameter,
 der leer ist und koennen die andere Regel anwenden.

  number_of(mt_string, c) = 0
  (c = d) -> number_of(cons(s, c), d) = succ(number_of(s, d))
  (c != d) -> number_of(cons(s, c), d) = number_of(s, d)
// number_of wird ebenfalls durch Vergleich der Zeichen vom letzten
 zum ersten ermittelt.

  last(cons(s, c)) = c
// last() muss fuer jeden String ein Zeichen liefern, das dem letzten
 Zeichen entspricht

  concat(s, mt_string) = s
// wenn an einen String ein leerer angehaengt wird, bleibt er unveraendert
  concat(s, cons(t, c)) = cons(concat(s, t), c)
// Anwendung des "Assoziativgesetzes" (s+(t+c)) = ((s+t)+c) auf die Verkettung von Strings und Zeichen



Preconditions: forall s: STRING
  pre(last(s)): not(is_mt(s))
// das letzte Zeichen eines leeren Strings kann nicht bestimmt werden

// Nachtrag:
// Was, wenn cons das neue Zeichen am Anfang einfuegt?! 
// Dann liefert last das erste Zeichen und alles andere funktioniert genauso. 
// Die Reihenfolge (vorwaerts oder rueckwaerts) der Zeichen  im STRING kann nicht
// bestimmt werden, das ist aber fuer die Benutzung des ADT egal.