i1prop.tex

% Diese Datei ist Teil des Buchs "Schreibe Dein Programm!"
% Das Buch ist lizenziert unter der Creative-Commons-Lizenz
% "Namensnennung - Weitergabe unter gleichen Bedingungen 4.0 International (CC BY-SA 4.0)"
% https://creativecommons.org/licenses/by-sa/4.0/deed.de

\chapter{Eigenschaften von Funktionen}
\label{cha:properties}

Woher wissen wir eigentlich, dass die Funktion, die wir geschrieben
haben, auch richtig funktioniert?  Wenn wir mit
Konstruktionsanleitungen arbeiten, stehen die Chancen nicht schlecht.
Die systematische Konstruktion hilft, von vornherein die Funktion
richtig zu schreiben.  Aber Kontrolle ist besser: Die Tests helfen,
etwaige Fehler zu finden.  Leider funktioniert das nicht immer, weil
jeder Tests nur ein einzelnes Beispiel überprüft.  Zumindest war das
bisher so.  In diesem Kapitel ändern wir das, in dem wir statt
einzelner Beispiele allgemeine \textit{Eigenschaften} von Funktionen
formulieren.  Aus diesen Eigenschaften können wir automatisch Tests
machen, die effektiver sind als die bisherigen, auf
\lstinline{check-expect} basierenden Tests.  Für hunderprozentige
Sicherheit können wir gelegentlich auch Eigenschaften mathematisch
beweisen.  Dieses Kapitel zeigt, wie es geht.

\section{Korrektheit und Tests}

\mentioncode{eigenschaften/heat-water.rkt}
%
Erinnerst Du Dich an die Funktion \lstinline{heat-water} aus
Abschnitt~\ref{sec:heat-water} auf Seite~\pageref{sec:heat-water}?
Die hatte ziemlich komplizierte Verzweigungen.  Dabei sind auch ein
paar Fehler passiert.  Zum Schluss hatten wir \lstinline{heat-water}
in zwei Funktionen aufgeteilt, \lstinline{heat->temperature} und
\lstinline{temperature->heat}.  Hier ist die erste davon, wobei wir
die Bedingungen in der Verzweigung etwas vereinfacht haben:
%
\indexvariable{heat->temperature}
\begin{lstlisting}
; Aus Wärme Temperatur berechnen
(: heat->temperature (real -> real))

(define heat->temperature
  (lambda (heat)
    (cond
      ((<= heat 0) heat)
      ((<= heat 80) 0)
      ((<= heat 180) (- heat 80))
      (else 100))))
\end{lstlisting}
%
Da waren außerdem ziemlich viele Testfälle:
%
\begin{lstlisting}
(check-expect (heat->temperature -50) -50)
(check-expect (heat->temperature 0) 0)
(check-expect (heat->temperature 20) 0)
(check-expect (heat->temperature 80) 0)
(check-expect (heat->temperature 81) 1)
(check-expect (heat->temperature 180) 100)
(check-expect (heat->temperature 200) 100)                                            
\end{lstlisting}
%
Die Testfälle haben eigentlich zwei Aufgaben:
%
\begin{enumerate}
\item Sie sollen als Beispiele die Funktion \emph{dokumentieren}.
\item Sie sollen außerdem sicherstellen, dass die Funktion
  \emph{korrekt} programmiert ist.
\end{enumerate}
%
Bei dieser Funktion allerdings gibt es bei beiden Aspekten Probleme.
Es sind so viele Testfälle und sie sind willkürlich und scheinbar
zufällig ausgewählt.  Das macht es Leserinnen und Lesern schwer, das
Wirkprinzip dahinter zu erkennen. Das führt dazu, dass uns (und
vielleicht auch Dich) das Gefühl nicht loslässt, dass bei den
Testfällen noch Fehler durchschlüpfen könnten.
%
\begin{aufgabeinline}
  Ändere die Funktion absichtlich so, dass sie einen Fehler enthält,
  und zwar so, dass trotzdem noch alle Testfälle erfolgreich laufen.  
\end{aufgabeinline}
%
Ein \lstinline{check-expect}-Test ist eben leider immer nur ein
einzelnes Beispiel, was seine Aussagekraft einschränkt.\footnote{In
  der professionellen Entwicklung heißt ein solcher Test
  \textit{Unit-Test}.\index{Unit-Test}.}  Oft ist eine allgemeine
Aussage die bessere Dokumentation.

In diesem Fall könnten wir zum Beispiel aussagen, dass es um Wasser
geht, die Temperatur also niemals größer als 100\si{\degree}C sein kann.  Das
geht nicht nur als Text, sondern auch als ein Stück Code:
%
\begin{lstlisting}
(<= (heat->temperature heat) 100)
\end{lstlisting}
%
Für sich genommen ergibt dieser Ausdruck keinen Sinn: \lstinline{heat}
ist nicht gebunden.  Wir brauchen noch den Zusatz, dass die Aussage
\emph{für alle} Werte von \lstinline{heat} gilt.  Also streng genommen
auch nicht für wirklich \emph{alle} Werte, nur alle Werte der Signatur
\lstinline{real}. Das können wir tatsächlich hinschreiben, mit Hilfe
einer neuen Form namens \lstinline{for-all}:
%
\begin{lstlisting}
(for-all ((heat real))
  (<= (heat->temperature heat) 100))
\end{lstlisting}
%
Das \lstinline{for-all}\indexvariable{for-all} 
bedeutet, wie der Name schon sagt, "<für alle">.  Da steht:
%
\begin{quote}
  Für \emph{alle} reellen Zahlen namens \lstinline{heat} muss das
  Ergebnis von \lstinline{(heat->temperature heat)} kleiner oder
  gleich 100 sein.
\end{quote}
%
"<Warum sind da doppelte Klammern um \lstinline{heat real}?"> wunderst
Du Dich vielleicht.  Das liegt daran, dass in dem äußeren Klammernpaar
mehrere Variablen vorkommen können, jede davon mit Signatur in einem
inneren Klammernpaar.  Dafür wird es noch Beispiele geben.
Abbildung~\ref{scheme:for-all} beschreibt genauer, wie
\lstinline{for-all}-Ausdrücke im Allgemeinen aufgebaut sind.

\begin{feature}{\lstinline{for-all}}{scheme:for-all}
  \lstinline{For-all}\indexvariable{for-all} ermöglicht das
  Formulieren von \textit{Eigenschaften\index{Eigenschaft}}.  Ein
  \lstinline{for-all}-Ausdruck hat die folgende allgemeine Form:
%
\begin{lstlisting}
(for-all (($\mathit{var}\sb{1}$ $\mathit{sig}\sb{1}$) $\ldots$ ($\mathit{var}\sb{n}$ $\mathit{sig}\sb{n}$)) $b$)
\end{lstlisting}
%
Dabei müssen die $\mathit{var}_i$ Variablen sein, die $\_i$ Signaturen und $b$ (der
Rumpf) ein Ausdruck, der entweder einen booleschen Wert oder eine
Eigenschaft liefert.  Der \lstinline{for-all}-Ausdruck hat als Wert eine
Eigenschaft, die besagt, dass $b$ gilt für \emph{alle} Werte der
$\mathit{var}_i$, welche die Signaturen $\mathit{sig}_i$ erfüllen.
\end{feature}

Das Ergebnis des \lstinline{for-all}-Ausdrucks wird in der REPL
etwas undurchsichtig angezeigt:
%
\begin{lstlisting}
(for-all ((heat real))
  (<= (heat->temperature heat) 100))
|\evalsto| #<:property>
\end{lstlisting}
%
Auf deutsch heißt "<property"> "<Eigenschaft">, denn 
es handelt sich um eine Eigenschaft der Funktion \lstinline{heat-temperature}.  

Diese Eigenschaft ersetzt nicht (immer) die Unit-Tests, ist aber eine
wertvolle Ergänzung der Dokumentation.

Sie kann außerdem auch dazu beitragen, die Korrektheit sicherzustellen.
Dazu wickeln wir um die Eigenschaft noch ein
\lstinline{check-property}:
%
\begin{lstlisting}
(check-property
 (for-all ((heat real))
   (<= (heat->temperature heat) 100)))
\end{lstlisting}
 %
\lstinline{Check-property} macht wie \lstinline{check-expect} oder
\lstinline{check-within} einen Testfall.

Da \lstinline{heat->temperature} korrekt programmiert ist, meldet
\lstinline{check-property} nur einen bestandenen Test.  Wozu
\lstinline{check-property} fähig ist, sieht man erst, wenn die
Funktion einen Fehler enthält.  Wenn wir zum Beispiel aus der $180$ eine
$280$ machen, dann erscheint folgende Meldung:
%
\begin{lstlisting}
Eigenschaft falsifizierbar mit heat = |\fbox{206}|
\end{lstlisting}
%
Wichtig: Wenn Du das bei Dir ausprobierst, kann die konkrete Zahl
eine andere sein.

Dickes Wort, "<falsifizierbar">\index{falsifizierbar}: Es heißt, das
Racket ein \textit{Gegenbeispiel} für die Eigenschaft gefunden hat.
Wir können das nachprüfen:
%
\begin{lstlisting}
(heat->temperature 206)
|\evalsto| 126
\end{lstlisting}
%
\ldots{} und 126 ist größer als 100.  Das Gegenbeispiel, das der
\lstinline{check-property}-Test gefunden hat, könnte, wenn wir den
Fehler nicht absichtlich gemacht hätte, dabei helfen, ihn zu finden
und zu beseitigen.

Abbildung~\ref{scheme:check-property} beschreibt den Aufbau von
\lstinline{check-property} genau.

\begin{feature}{\lstinline{check-property}}{scheme:check-property}

\lstinline{Check-property}\indexvariable{check-property}
testet eine Eigenschaft analog zu \lstinline{check-expect}.  Eine
\lstinline{check-property}"=Form sieht so aus:
%
\begin{lstlisting}
(check-property $e$) 
\end{lstlisting}
%
$e$ ist ein Ausdruck, der eine Eigenschaft liefern muss~-- in der Regel
also ein \lstinline{for-all}-Ausdruck.  Die Form testet dann diese
Eigenschaft.  (Mehr dazu im nächsten Abschnitt.)

\lstinline{Check-property} funktioniert nur für Eigenschaften, bei
denen aus den Signaturen sinnvoll Werte generiert werden können.  Dies
ist für die meisten Signaturen der Fall, aber nicht für
\lstinline{any} und Signaturvariablen definiert wurden.
\end{feature}

\begin{aufgabeinline}
  Mache noch absichtlich ein paar weitere Fehler in
  \lstinline{heat->temperature}.  Welche davon werden von dem
  \lstinline{check-property}-Test gefunden und welche nicht?
\end{aufgabeinline}

Da \lstinline{check-property} eine Eigenschaft testet, heißt diese
Technik auch \textit{property-based testing}.\index{property-based
  testing}  Die werden wir im Laufe dieses Kapitels noch auf andere
Funktionen anwenden.

\section{Wie \lstinline{check-property} funktioniert}

Zunächst machen wir aber einen kleinen Exkurs: Was passiert
bei so einem \lstinline{check-property}-Test?

Toll wäre natürlich, wenn dieser mit Gewissheit sagen könnte, was die
Eigenschaft besagt: Dass zum Beispiel die Temperatur wirklich für
\emph{alle} Eingaben höchstens $100$ ist.  Das ist im allgemeinen leider
unmöglich.\footnote{Dass das unmöglich ist, wurde mathematisch
  bewiesen und als \textit{Satz von Rice} festgehalten.  Der ist Thema
  in der theoretischen Informatik.}  In manchen Fällen ist es trotzdem
möglich, Eigenschaften von Funktionen formal zu beweisen.  (Dazu mehr in
Abschnitt~\ref{sec:eigenschaften-beweisen} auf
Seite~\pageref{sec:eigenschaften-beweisen}.)

\lstinline{Check-property} kann also nicht 
beweisen, dass eine Eigenschaft gilt.  Stattdessen führt es Stichproben durch: Dafür
wählt es für die Signaturen zufällig Werte aus, und
wiederholt diesen Prozess, um so aus einem Testfall viele individuelle
Tests zu machen~-- typischerweise $100$.

Die Verwendung des Begriffs "<zufällig"> ist in diesem Zusammenhang in
der Informatik so üblich, ein besseres Wort wäre aber "<chaotisch">.
Tatsächlich produziert \lstinline{check-property} bei jedem Durchlauf
des Programms die gleichen Tests.

Die Technik des \textit{property-based testing}, also zunächst
allgemeine Eigenschaften zu formulieren und für diese dann Testfälle
zu erzeugen, ist ursprünglich unter dem Namen \textit{QuickCheck}
veröffentlicht worden~\cite{ClaessenHughes2000} und war ein
großer Durchbruch bei der Effektivität von automatischen Tests.

\section{Mehr Eigenschaften und inexakte Zahlen}
\label{sec:inexakt}

Es geht weiter mit \lstinline{heat-water}:
\lstinline{Heat->temperature} ist nur eine Hilfsfunktion dafür,
zusammen mit \lstinline{temperature->heat}.  Auch hier könnten wir
eine Eigenschaft aufschreiben, die etwas über den Zahlenbereich
aussagt, der aus der Funktion herauskommt.

Allerdings gibt es noch eine weitaus ergiebigere Eigenschaft:
\lstinline{temperature->heat} soll ist ja gerade
\lstinline{heat->temperature} "<umdrehen">.  Daraus können wir
folgende Eigenschaft beziehungsweise folgenden Test machen:
%
\begin{lstlisting}
(check-property
 (for-all ((temp real))
   (= (heat->temperature (temperature->heat temp))
      temp)))
\end{lstlisting}
%
Der besagt also dass, wenn eine Temperatur in Wärme gewandelt wird und
wieder zurück in eine Temperatur, dass dann das gleiche herauskommen
soll.  Leider schlägt der Test fehl:
%
\begin{lstlisting}
Eigenschaft falsifizierbar mit temp = |\fbox{0}|
\end{lstlisting}
%
Wir können in der REPL für \lstinline{temp} mal $0$ einsetzen:
%
\begin{lstlisting}
(heat->temperature (temperature->heat 0))
|\evalsto| cond: alle Bedingungen ergaben #f
\end{lstlisting}
%
Da war doch was?  Vielleicht erinnerst Du Dich: Eine Temperatur von
$0$\si{\degree}C kann nicht eindeutig einer Wärmezahl zugeordnet werden,
die kann zwischen $0$ und $80$ liegen.  Deshalb weigert sich auch
\lstinline{heat->temperature}, für die Eingabe $0$ ein Ergebnis zu
produzieren.  Wir müssen also unseren Test anpassen, so dass da steht
"<für alle reellen Zahlen \emph{außer} $0$">.

Das geht folgendermaßen:
%
\begin{lstlisting}
(check-property
 (for-all ((temp real))
   (==> (not (= temp 0))
        (= (heat->temperature (temperature->heat temp))
           temp))))
\end{lstlisting}
%
Der Pfeil \lstinline{==>} ist neu und funktioniert nur im Kontext
einer Eigenschaft: Er bedeutet "<gilt unter der Voraussetzung">.
Abbildung~\ref{feature:implication} erklärt im Detail, wie die Form
funktioniert.  Hier steht also, dass die Gleichung nur gelten muss
unter der Voraussetzung, dass \lstinline{temp} nicht $0$ ist.

\begin{feature}{Voraussetzung bei Eigenschaften}{feature:implication}
  In einer Eigenschaft steht die Form
\begin{lstlisting}
(==> $p$ $e$)
\end{lstlisting}
  dafür, dass die Eigenschaft $e$ nur dann gelten muss, wenn der
  Ausdruck $p$ den Wert \lstinline{#t} ergibt.

  Bei einer \lstinline{==>}-Form generiert \lstinline{check-property}
  nur solche Tests, bei denen $p$ \lstinline{#t} ergibt.
\end{feature}
%
\begin{quote}
\noindent \emph{Anmerkung:} Du könntest die Eigenschaft oben
auch mit \lstinline{if} statt \lstinline{==>} hinschreiben:
%
\begin{lstlisting}
(check-property
 (for-all ((temp real))
   (if (= temp 0))
       #t
       (= (heat->temperature (temperature->heat temp))
          temp)))
\end{lstlisting}
%
Bedeuten würde die Eigenschaft so das gleiche.  Allerdings behandelt
\lstinline{check-property} diese Schreibweise anders, nämlich
schlechter.  Wenn \lstinline{check-property} 100 Tests generiert, dann
werden alle, bei denen \lstinline{temp} $0$ ist, als Erfolg gewertet,
obwohl da eigentlich nichts getestet wird.  Wenn für (hypothetisch)
drei von den Tests \lstinline{temp} $0$ ist, dann werden also nur 97
richtige Tests durchgeführt.

In der Variante mit \lstinline{==>} stellt
\lstinline{check-property} sicher, dass tatsächlich $100$ Tests
durchgeführt werden, bei denen \lstinline{temp} nicht $0$ ist.  Damit
wird mehr getestet.
\end{quote}
%
Wenn wir den Testfall laufen lassen, gibt es allerdings eine
merkwürdige Überraschung:
%
\begin{lstlisting}
Eigenschaft falsifizierbar mit temp = #i24.571428571428573
\end{lstlisting}
%
Wie schon gesagt, die konkrete Zahl kann anders aussehen, aber es geht
um das merkwürdige \mbox{\lstinline{#i}}.  Das steht für "<inexakt">, weil es
sich um eine sogenannte \textit{inexakte Zahl}\index{inexakte Zahl}
handelt.  Solche Zahlen werden von DrRacket (und so gut wie allen
anderen Programmiersprachen) verwendet, um die Ergebnisse von
Berechnungen darzustellen, die (zumindest mit vertretbarem Aufwand)
nicht ganz genau durchgeführt werden können.

Bisher ging in diesem Buch alles noch ganz genau, weil unsere
Programme bisher intern exakte Bruchrechnung verwendet haben.  Um so
eine inexakte Zahl zu berechnen, kannst Du zum Beispiel das hier in
der REPL ausprobieren, um die Quadratwurzel ("<square root">) von 2
auszurechnen:
%
\begin{lstlisting}
(sqrt 2)
|\evalsto| #i1.4142135623730951
\end{lstlisting}
%
Die Wurzel von 2 hat unendlich viele Nachkommestellen, weswegen Racket
davon nur einige ausrechnet und rundet.  Und damit wir und Du wissen,
dass gerundet wurde, steht das \lstinline{#i} davor.

Das mit dem Runden ist sogar noch komplizierter, als es scheint: Es
wird nämlich \emph{binär} gerechnet.  Wie genau abläuft, ist ziemlich
kompliziert und würde ein weiteres Buch füllen.  Mehr zu dem Thema
findet sich zum Beispiel im Standardwerk von David
Goldberg~\cite{Goldberg1991}.

Aber was ist denn nun genau bei unserer Eigenschaft passiert?  Wir
können die \lstinline{#i}-Zahl von Hand in die Eigenschaft einsetzen
und in der REPL auswerten:
%
\begin{lstlisting}
(heat->temperature (temperature->heat #i24.571428571428573))
|\evalsto| #i24.57142857142857
\end{lstlisting}
%
Du kannst sehen, dass offensichtlich beim Rechnen gerundet wurde, und
zwar bei der letzten Nachkommastelle.  Das erscheint Dir vielleicht
merkwürdig, weil in 
\lstinline{temperature->heat} doch ausschließlich addiert und
subtrahiert wird~-- da ist keine Spur von "<Runden">.  Wenn wir das
\lstinline{#i} weglassen, wird auch exakt gerechnet:\footnote{Falls Du
  es mal mit einer der anderen Sprachen zu tun hast, die beim
  Racket-System dabei sind: Bei den meisten von ihnen wird, anders als
  hier, jede Zahl mit Dezimalpunkt als inexakt behandelt.}
%
\begin{lstlisting}
(heat->temperature (temperature->heat 24.571428571428573))
|\evalsto| 24.571428571428573
\end{lstlisting}
%
Das liegt daran, dass "<Inexaktheit"> ansteckend ist: Wenn beim Aufruf
einer Rechenfunktion wie \lstinline{+} oder \lstinline{*} auch nur
eine Eingabe inexakt ist, wird gerundet.

Weil diese Rundung manchmal überraschend ist, weigert sich übrigens
\lstinline{check-expect}, inexakte Zahlen zu vergleichen.
%
\begin{aufgabeinline}
  Probier's aus: \lstinline{(check-expect #i1 #i1)}
\end{aufgabeinline}
%
Bei unserer Eigenschaft
haben für \lstinline{temp} die Signatur \lstinline{real} angegeben: In
dieser Signatur sind auch inexakte Zahlen enthalten, deshalb nimmt da
das Problem seinen Anfang.  Wir können es auf zwei Arten angehen:
%
\begin{itemize}
\item Wir ersetzen in der Eigenschaft die Signatur \lstinline{real}
  durch \lstinline{rational}.  In \lstinline{rational} sind keine
  inexakten Zahlen drin.  Das hat allerdings den Nachteil, dass auch
  nur auf exakten Zahlen getestet wird, obwohl die Funktionen auch auf
  inexakten Zahlen funktionieren.
\item Wir berücksichtigen den Effekt der Rundung, indem wir die Bedingung
  in der Eigenschaft etwas aufweichen.
\end{itemize}
%
Wir machen letzteres und fordern nur, dass der Abstand zwischen echtem
und erwartetem Ergebnis einen bestimmten Betrag nicht überschreitet:
%
\begin{lstlisting}
(check-property
 (for-all ((temp real))
   (==> (not (= temp 0))
        (<= (abs
             (- (heat->temperature (temperature->heat temp))
                temp))
            0.0000001))))
\end{lstlisting}
%
Zur Erinnerung: Die eingebaute Funktion \lstinline{abs} berechnet den
Absolutbetrag, dreht also bei negativen Zahlen das Vorzeichen um,
siehe Abschnitt~\ref{func:abs} auf Seite~\pageref{func:abs}.

Leider schlägt der Test immer noch fehl, zum Beispiel mit folgender
Ausgabe:
%
\begin{lstlisting}
Eigenschaft falsifizierbar mit temp = 105
\end{lstlisting}
%
Das können wir in der REPL ausprobieren:
%
\begin{lstlisting}
(heat->temperature (temperature->heat 105))
|{\color{red}cond: alle Bedingungen ergaben \#f}|
\end{lstlisting}
%
Das liegt daran, dass \lstinline{temperature->heat} nur für
Temperaturen bis 100\si{\degree}C funktioniert: Wasser kann ja nicht
heißer werden.  Wir müssen also unsere Vorbedingung erweitern:
%
\begin{lstlisting}
(check-property
 (for-all ((temp real))
   (==> (and (not (= temp 0))
             (< temp 100))
        (<= (abs
             (- (heat->temperature (temperature->heat temp))
                temp))
            0.0000001))))
\end{lstlisting}
%
Dieser Text drückt ganz gut aus, wie \lstinline{heat->temperature} und
\lstinline{temperature->heat} zueinander stehen: Die eine dreht die
andere um, zumindest ungefähr.  In der Mathematik heißt es, dass die
eine Funktion die \textit{Inverse} andere anderen Funktion
ist.\index{Inverse}

\begin{aufgabeinline}
  Versuche, den letzten \lstinline{check-property}-Test
  auszutricksen.  Anstatt kleine Fehler einzuführen, versuche es mal
  mit ganz anderen Funktionen, die gar nichts mit Wassertemperaturen
  zu tun haben, aber trotzdem die obige Eigenschaft haben.
\end{aufgabeinline}
%
Die Aufgabe zeigt, dass Eigenschaften kein Garant für Korrektheit
sind: Genau wie bei Unit-Tests auch braucht es oft mehrere davon oder
zusätzliche \lstinline{check-expect}-Tests, um für genug Sicherheit zu
sorgen.

Die Technik aus der Aufgabe ist dabei hilfreich: Überlege, wie Du
einen Testfall durch falsche Funktionen austricksen kannst.  Füge dann
Testfälle hinzu, die diese Fehler aufspüren.

% FIXME: Konstruktionsanleitung?

% FIXME Korrektheit Gürteltiere

\section{Relationale Probleme}

\mentioncode{eigenschaften/sort.rkt}
%
Die Eigenschaften für \lstinline{heat-water} hätten wir auch durch
eine (lange) Reihe von \lstinline{check-expect}-Tests ersetzen können.
Die Eigenschaften sind da hilfreich, aber nicht unverzichtbar.  Aber
es gibt Funktionen, bei denen Unit-Tests grundsätzlich nicht das
richtige sind, nämlich solche, die sogenannte \textit{relationale
  Probleme} lösen.  Um die geht es in diesem Abschnitt.

Wir schreiben zunächst eine solche Funktion, um das Konzept zu
erklären: Sie soll die Mitglieder einer Band nach Alter sortieren.

Hier sind Daten- und Record-Definition für ein Bandmitglied:
%
\begin{lstlisting}
(define-record band-member
  make-band-member
  (band-member-name string)
  (band-member-born natural))
\end{lstlisting}
%
Und hier die konkrete Band dazu (Stand 2021):
%
\indexvariable{axl (make-band-member "Axl Rose" 1962))}
\indexvariable{duff (make-band-member "Duff McKagan" 1964))}
\indexvariable{slash (make-band-member "Slash" 1965))}
\indexvariable{dizzy (make-band-member "Dizzy Reed" 1963))}
\indexvariable{richard (make-band-member "Richard Fortus" 1966))}
\indexvariable{frank (make-band-member "Frank Ferrer" 1966))}
\indexvariable{melissa (make-band-member "Melissa Reese" 1990))}
\indexvariable{guns-n-roses}
\begin{lstlisting}
(define axl (make-band-member "Axl Rose" 1962))
(define duff (make-band-member "Duff McKagan" 1964))
(define slash (make-band-member "Slash" 1965))
(define dizzy (make-band-member "Dizzy Reed" 1963))
(define richard (make-band-member "Richard Fortus" 1966))
(define frank (make-band-member "Frank Ferrer" 1966))
(define melissa (make-band-member "Melissa Reese" 1990))

(define guns-n-roses
  (list axl duff slash dizzy richard frank melissa))
\end{lstlisting}
%
Wir machen das mit einem
einfachen, wenn auch ineffizienten Verfahren namens
\textit{Insertionsort}\index{Insertionsort}:
Die Sortierfunktion arbeitet mit einer sortierten Liste als
Akkumulator.  Diese ist anfänglich leer, und die Funktion fügt jeweils
ein Element aus der Eingabeliste hinzu, indem sie dies an der
richtigen Stelle einfügt.
%
% Die Funktion soll sowohl aufsteigend als auch absteigend oder nach
% einem anderen Kriterium sortieren können.  Das machen wir ähnlich wie
% bei den Suchbäumen in Abschnitt~\ref{sec:suchbaeume} auf
% Seite~\pageref{sec:suchbaeume}, wo wir über die Funktionen abstrahiert
% haben, die Markierungen im Baum vergleichen.  Bei den Suchbäumen waren
% das zwei Funktionen für \lstinline{=} und \lstinline{<}, hier
% kombinieren wir beides in eine Funktion wie \lstinline{<=}.
% FIXME: Halbordnung irgendwann?
%
%
Wir schreiben zunächst eine Hilfsfunktion zum Einfügen eines Elements.
Das Testen heben wir uns ausnahmsweise bis zum Testen der
Sortierfunktion auf.  Kurzbeschreibung,
Signatur, Gerüst und Schablone:
%
\indexvariable{insert}
\begin{lstlisting}
; Bandmitglied in eine sortierte Liste einfügen
(: insert
   (band-member (list-of band-member) -> (list-of band-member)))

(define insert
  (lambda (band-member list)
    (cond
      ((empty? list) ...)
      ((cons? list)
       ...
       (first list)
       (insert band-member (rest list))
       ...))))
\end{lstlisting}
%
Im ersten Fall fügt die Funktion eine leere Liste ein: Das Ergebnis
sollte dann die Liste mit \lstinline{element} als einzigem Element
sein.  Im zweiten Fall ist noch unklar, wo \lstinline{band-member}
eingefügt wird, vor oder nach \lstinline{(first list)}.  Die Funktion
muss die beiden Geburtsjahre miteinander vergleichen:
%
\begin{lstlisting}
(define insert
  (lambda (band-member list)
    (cond
      ((empty? list) (cons band-member empty))
      ((cons? list)
       (if (<= (band-member-born band-member)
               (band-member-born (first list)))
           (cons band-member list)
           (cons (first list)
                 (insert band-member (rest list))))))))
\end{lstlisting}
%
Mit Hilfe von \lstinline{insert} bauen wir nun die Funktion
\lstinline{sort-band}.  Kurzbeschreibung, Signatur und Unit-Test:
%
\begin{lstlisting}
; Band nach Alter sortieren
(: sort-band ((list-of band-member) -> (list-of band-member)))

(check-expect (sort-band guns-n-roses)
              (list axl dizzy duff slash richard frank melissa))
\end{lstlisting}
%
Hier die Schablone für die Funktion~-- mit Akkumulator:
%
\begin{lstlisting}
(define sort-band
  (lambda (list0)
    ; Invariante: ...
    (define accumulate     
      (lambda (list acc)
        (cond
          ((empty? list) ...)
          ((cons? list)
           (accumulate (rest list)
                       ... (first list) ... acc ...)))))
    (accumulate list0 ...)))
\end{lstlisting}
%
Beim Akkumulieren enthält \lstinline{list} die schon gesehenen
Elemente aus \lstinline{list0}, und zwar sortiert.  Daraus können wir
eine Invariante formulieren:
%
\begin{lstlisting}
    ; Invariante: list enthält die Bandmitglieder
    ; zwischen list0 und list, sortiert.
\end{lstlisting}
%
Damit können wir die Lücken füllen: \lstinline{acc} ist beim ersten
Aufruf leer.  Wenn \lstinline{list} leer ist, dann ist \lstinline{acc}
das gewünschte Endergebnis.  Das neue Zwischenergebnis berechnet die
Funktion mit Hilfe von \lstinline{insert}:
%
\indexvariable{sort-band}
\begin{lstlisting}
(define sort-band
  (lambda (list0)
    ; Invariante: list enthält die Bandmitglieder
    ; zwischen list0 und list, sortiert.
    (define accumulate     
      (lambda (list acc)
        (cond
          ((empty? list) acc)
          ((cons? list)
           (accumulate (rest list)
                       (insert (first list) acc))))))
    (accumulate list0 empty)))
\end{lstlisting}
%
Fertig! Halt, da ist noch ein kleines Problem:
%
\begin{verbatim}
Der tatsächliche Wert 
#<list
 #<record:band-member "Axl Rose" 1962>
 #<record:band-member "Dizzy Reed" 1963>
 #<record:band-member "Duff McKagan" 1964>
 #<record:band-member "Slash" 1965>
 #<record:band-member "Frank Ferrer" 1966>
 #<record:band-member "Richard Fortus" 1966>
 #<record:band-member "Melissa Reese" 1990>>
ist nicht der erwartete Wert 
#<list
 #<record:band-member "Axl Rose" 1962>
 #<record:band-member "Dizzy Reed" 1963>
 #<record:band-member "Duff McKagan" 1964>
 #<record:band-member "Slash" 1965>
 #<record:band-member "Richard Fortus" 1966>
 #<record:band-member "Frank Ferrer" 1966>
 #<record:band-member "Melissa Reese" 1990>>.
\end{verbatim}
%
Woran liegt's?  Richard Fortus und Frank Ferrer sind im selben Jahr
geboren.  Der Unit-Test nimmt an, dass Fortus vor Ferrer
einsortiert wird, aber \lstinline{sort-band} macht es aber genau
umgekehrt.  Deswegen ist \lstinline{sort-band} nicht verkehrt: Es gibt
einfach mehrere korrekte Antworten.

Der Unit-Test ist also ungünstig, selbst wenn wir die Reihenfolge so
wählen, dass er nicht fehlschlägt.  Wenn wir die Suchfunktion
irgendwann mal ändern, kann
sich die Reihenfolge ändern und der Test schlägt wieder fehl, auch
wenn die Funktion korrekt ist.

Da es für \lstinline{sort-band} für eine gegebene Eingabe mehr als ein
korrektes Ergebnis geben kann, sprechen wir von einem "<relationalen
Problem">:\index{relationales Problem} Es steht nicht das präzise
Ergebnis fest, nur die Beziehung ("<Relation">) zwischen Ein- und
Ausgabe.  Und um die zu beschreiben, ist eine Eigenschaft das richtige
Mittel.  Wie könnte eine sinnvolle Eigenschaft einer Funktion
aussehen, die sortiert?
Nun, dass die Ausgabe sortiert ist.  Um das festzustellen, schreiben
wir eine Funktion:
%
\begin{lstlisting}
; Band sortiert?
(: band-sorted? ((list-of band-member) -> boolean))
\end{lstlisting}
%
Die Tests lassen unterschiedliche Reihenfolgen zu, solange sie
sortiert sind:
%
\begin{lstlisting}
(check-expect
  (band-sorted? (list axl dizzy duff slash frank richard melissa))
  #t)
(check-expect
  (band-sorted? (list axl dizzy duff slash richard frank melissa))
  #t)
(check-expect
  (band-sorted? (list dizzy axl duff slash richard frank melissa))
  #f)
(check-expect
  (band-sorted? (list axl dizzy duff richard slash frank melissa))
  #f)
\end{lstlisting}
%
Hier sind Gerüst und Schablone:
%
\begin{lstlisting}
(define band-sorted?
  (lambda (list)
    (cond
      ((empty? list) ...)
      ((cons? list)
       ... (first list) ...
       ... (band-sorted? (rest list) ...)))))
\end{lstlisting}
%
Der \lstinline{empty}-Fall ist einfach: Eine leere Liste ist sortiert.
Im \lstinline{cons}-Fall ist es etwas schwieriger.  Um die Reihenfolge
zu überprüfen, müssen wir zwei Elemente der Liste miteinander
vergleichen, da ist aber nur \lstinline{(first list)}.  Wir brauchen
also noch das zweite Element.  Das gibt es nur bei Listen mit mehr als
einem Element, weswegen wir eine zweite Verzweigung brauchen:
%
\begin{lstlisting}
(define band-sorted?
  (lambda (list)
    (cond
      ((empty? list) #t)
      ((cons? list)
       (cond
         ((empty? (rest list)) ...)
         ((cons? (rest list))
          ...
          (first list)
          (first (rest list))))
          (band-sorted? (rest list))
          ...))))
\end{lstlisting}
%
Der innere \lstinline{empty}-Fall ist die Liste mit einem Element: Die
ist auch immer sortiert.  Im \lstinline{cons}-Fall schließlich können
wir die beiden ersten Elemente vergleichen:
%
\indexvariable{band-sorted?}
\begin{lstlisting}
(define band-sorted?
  (lambda (list)
    (cond
      ((empty? list) #t)
      ((cons? list)
       (cond
         ((empty? (rest list)) #t)
         ((cons? (rest list))
          (and (<= (band-member-born (first list))
                   (band-member-born (first (rest list))))
               (band-sorted? (rest list)))))))))
\end{lstlisting}
%
Diese Funktion können wir nun benutzen, um aufzuschreiben, dass
\lstinline{sort-band} immer sortierte Listen produziert:
%
\begin{lstlisting}
(check-property
 (for-all ((list (list-of band-member)))
   (band-sorted? (sort-band list))))
\end{lstlisting}
%
Diese Eigenschaft bringt auf den Punkt, was \lstinline{sort-band}
ausmacht, nämlich dass sie sortierte Listen produziert.  Sie ist also
schon mal eine gute Dokumentation.

Ist sie auch ein guter Testfall?  Vielleicht hast Du ein mulmiges
Gefühl, dass wir für den Test von \lstinline{sort-band} eine weitere
selbstgeschriebene Funktion benutzt haben, die fast ebenso kompliziert
ist wie \lstinline{sort-band} selbst.  Was, wenn wir in
\lstinline{band-sorted?} einen Fehler gemacht haben, und zwar so,
dass der Eigenschafts-Testfall dann einen Fehler in
\lstinline{sort-band} nicht mehr findet.  Das ist natürlich
theoretisch möglich, ist aber unwahrscheinlich und wird umso
unwahrscheinlicher, je mehr Testfälle mit aussagekräftigen
Eigenschaften dazukommen.

Diese Eigenschaften sind eine Form von Redundanz,\index{Redundanz}
analog dazu, bei Gebäuden lieber die tragenden Wände etwas stärker zu
machen als unbedingt notwendig.  Ob diese Redundanz die Arbeit wert
ist, eine Funktion wie \lstinline{band-sorted?} zu schreiben, die nur
für das Testen gut sind, hängt vom Einzelfall ab: Je wichtiger die
Korrektheit der Funktion und je komplizierter sie ist, desto größer
ist der Wert solcher Testfälle.

Trotzdem kann man die obige Eigenschaft austricksen, ziemlich einfach
sogar:
%
\begin{lstlisting}
(define sort-band
  (lambda (list0)
    empty))
\end{lstlisting}
%
Das ist natürlich ein bisschen gemein.  Aber die Funktion, die den
Testfall austrickst, ist einfacher, als die richtige Funktion.  Es ist
also einfacher, es falsch zu machen als richtig.  Deshalb sollten wir
nach weiteren Eigenschaften suchen, die solche einfachen aber falschen
Lösungen finden.  Zum Beispiel könnten wir fordern, dass die
Ausgabeliste genauso lang ist wie die Eingabe:
%
\begin{lstlisting}
(check-property
 (for-all ((list (list-of band-member)))
   (= (length (sort-band list))
      (length list))))
\end{lstlisting}
%
\begin{aufgabeinline}
  Die folgende Version von \lstinline{sort-band} besteht die
  bisherigen Testfälle:
  %
\begin{lstlisting}
(define sort-band
  (lambda (list)
    (cond
      ((empty? list) empty)
      ((cons? list)
       (map (lambda (band-member)
              (first list))
            list)))))
\end{lstlisting}
  %
  Kannst Du einen Testfall schreiben, der den Fehler in dieser
  Funktion findet?
\end{aufgabeinline}

% FIXME:
% - viele check-expect-Tests ersetzen
% - relationale Probleme
% - Invarianten
% - häufig vorkommende Eigenschaften

\section{Konstruktionsanleitungen für Testfälle?}
\label{sec:ka-testfaelle}

Die bisherigen Beispiele für Testfälle mit Eigenschaften haben Dich
hoffentlich überzeugt, dass es eine gute Idee ist, solche Testfälle zu
schreiben.  Aber \emph{wie} geht das eigentlich bei der nächsten
Funktion, die getestet werden soll?  Toll wären
Konstruktionsanleitungen analog zu denen für Funktionen, die zeigen,
wie wir Eigenschaften aus der Signatur der zu testenden Funktion
herleiten können.  Das hätte zumindest bei den Funktionen der
bisherigen Abschnitte dieses Kapitels nicht funktioniert.

Trotzdem gibt es ein paar Dinge, die Du probieren kannst, wenn Du
Eigenschaften für eine neue Funktion formulieren willst:
%
\begin{enumerate}
\item Benutze das Wissen über die Größen Deines Problems.

  Beispiele:

  \begin{itemize}
    \item Wenn es um die Temperatur von Wasser geht, weißt Du,
    dass die Temperatur nicht größer als $100$\si{\degree}C sein kann.
  \item Du weißt, das
    die Ausgabe einer Sortierfunktion sortiert sein sollte.
  \end{itemize}
\item Oft gehören zu einem Problem mehrere Funktionen, die auf
  bestimmte Art und Weise zusammenarbeiten.  Schreibe auf, wie diese
  Zusammenarbeit aussieht.

  Beispiel: \lstinline{Temperature->heat} dreht
  \lstinline{heat->temperature} um.
\item Versuche, die bestehenden Eigenschaften durch einfache aber
  fehlerhafte Varianten Deiner Funktion auszutricksen.
  Suche dann nach
  Eigenschaften, die das Austricksen verhindern.

  Beispiel: Die leere Liste als Resultat \lstinline{sort-band} ist
  immer sortiert, aber trotzdem falsch.
\end{enumerate}
%
Abschnitt~\ref{sec:algebraische-eigenschaften} auf
Seite~\pageref{sec:algebraische-eigenschaften} wird diese Liste noch
ergänzen um Eigenschaften, die tatsächlich mit den Signaturen der zu
testenden Funktionen zu tun haben.

\section{Suchbäume testen}
\label{sec:suchbaeume-testen}

\mentioncode{baeume/binary-tree.rkt}
%
In Abschnitt~\ref{sec:balanced-search-trees} auf
Seite~\pageref{sec:balanced-search-trees} haben wir die Funktion
\lstinline{balanced-search-tree-insert}, und die war ziemlich
kompliziert.  Vielleicht ging es Dir wie uns~-- wir hatten ein etwas
mulmiges Gefühl, ob die Funktion auch wirklich korrekt ist.
Sie hat ziemlich viele Verzweigungen, nicht nur in der Funktion selbst
sondern auch in der Hilfsfunktion \lstinline{make-balanced-node}.
Dass die Testfälle wirklich jede mögliche Form von Suchbaum testen,
ist ziemlich unwahrscheinlich.

Eine weitere Schwierigkeit beim Testen von
\lstinline{balanced-search-tree-insert} ist, dass die Funktion ein
relationales Problem löst: Es gibt mehr als ein korrektes
Ergebnis. Bei einem Testfall mit \lstinline{check-expect}-,
der ein bestimmtes Ergebnis von 
\lstinline{balanced-search-tree-insert} erwartet, kann es sein, dass
die Funktion ein anderes, aber trotzdem korrektes Ergebnis liefert.
Der Testfall schlägt dann fehl, und die Suche nach der Ursache ist
mühsam.

Aber mit ein paar Eigenschaften können wir (hoffentlich) das mulmige
Gefühl beseitigen und unser Vertrauen in die Funktion erhöhen.  Der
vorige Abschnitt hatte einige Vorschläge, wie wir vorgehen können.
Der erste Vorschlag war:
%
\begin{quote}
  Benutze das Wissen über die Größen Deines Problems.
\end{quote}
%
Die Größe unseres Problems ist hier der balancierte Suchbaum.  In dem
Begriff steckt schon ziemlich viel Wissen:
%
\begin{enumerate}
\item Das Ergebnis von \lstinline{balanced-search-tree-insert} sollte ein
  sortierter Baum sein, bei dem alle Markierungen im linken Teilbaum
  eines Knotens kleiner sein sollte als die Markierung des Knotens.
\item Die Bäume sind größenannotiert: Die Größenannotation sollte auch
  stimmen, also bei jedem Knoten die tatsächliche Größe des Baums
  darunter wiedergeben.
\item Schließlich und endlich sollte der balancierte Suchbaum
  natürlich auch \emph{balanciert} sein.
\end{enumerate}
%
Wir fangen mal mit dem zweiten Punkt an, und überlassen Dir danach den
ersten als Übungsaufgabe.  Um zu überprüfen, ob die Größenannotation
stimmt, müssen wir die Annotation jeden Knoten des Baums betrachten.
Dafür brauchen wir eine Hilfsfunktion.  Sie hat folgende
Kurzbeschreibung und Signatur:
%
\begin{lstlisting}
; Stimmt die Größenannotation am Suchbaum?
(: proper-sized-search-tree? ((sized-search-tree-of %a) -> boolean))
\end{lstlisting}
%
Hier sind zwei einfache Testfälle dafür:
%
\begin{lstlisting}
(check-expect (proper-sized-search-tree? sized-search-tree1) #t)
(check-expect (proper-sized-search-tree?
               (make-sized-search-tree
                = <
                (make-sized-node
                 5
                 (make-node (make-sized-label 5 3) #f #f)
                 (make-node (make-sized-label 2 7) #f #f))))
               #f)
\end{lstlisting}              
%
Nur zwei popelige Testfälle, magst Du einwenden, mehr wären sicher
besser.  Allerdings werden wir sie noch in
\lstinline{check-property}-Tests zusammen mit
\lstinline{balanced-search-tree-insert} aufrufen und wir hoffen, dass
dies die benötigte Redundanz schafft und unser Vertrauen in die
Korrektheit von
\lstinline{balanced-search-tree-insert} erhöht.  Aber ist diese
Hoffnung auch berechtigt?  Wir können uns zwei Szenarien vorstellen,
in denen das nicht der Fall ist, also der Testfall keine Fehler
findet, obwohl welche vorhanden sind:
%
\begin{itemize}
\item \lstinline{Proper-sized-search-tree?} liefert \emph{immer}
  \lstinline{#t}, dann ist jeder Testfall damit nutzlos.  Das haben
  wir aber durch den einen \lstinline{check-expect}-Testfall
  ausgeschlossen.
\item \lstinline{Proper-sized-search-tree?} ist zufällig genau so fehlerhaft,
  dass die Funkktion inkorrekte Resultate aus
  \lstinline{balanced-search-tree-insert} als korrekt absegnet.
  Allerdings ist
  \lstinline{proper-sized-search-tree?} viel einfacher ist als
  \lstinline{balanced-search-tree-insert} und Fehler dort
  unwahrscheinlicher.  Durch die Absicherung der einen durch die
  andere Funktion haben wir die Redundanz\index{Redundanz} im
  Gesamtsystem erhöht.
\end{itemize}
%
Hier das Gerüst für die Funktion:
%
\begin{lstlisting}
(define proper-sized-search-tree?
  (lambda (search-tree)
    ...))
\end{lstlisting}
%
Wir gehen beim Rumpf vor wie bei der Funktion
\lstinline{sized-search-tree-member?} auf
Seite~\pageref{func:sized-search-tree-member}. Der eigentliche Baum
steckt in dem \lstinline{search-tree}-Record.  Den extrahieren
wir und lassen die eigentliche Arbeit von einer internen Hilfsfunktion erledigen.
%
\begin{lstlisting}
(define proper-sized-search-tree?
  (lambda (search-tree)
    (define proper?
      (lambda (tree)
        ...))
    (proper? (sized-search-tree-tree search-tree))))
\end{lstlisting}
%
Hier die Schablone:
%
\begin{lstlisting}
(define proper-sized-search-tree?
  (lambda (search-tree)
    (define proper?
      (lambda (tree)
        (cond
          ((node? tree)
           ...
           (proper? (node-left-branch tree))
           (proper? (node-right-branch tree))
           (node-label tree)
           ...)
          (else ...))))
  (proper? (sized-search-tree-tree search-tree))))
\end{lstlisting}
%
Ein paar Lücken können wir schon füllen: Bei einem Blatt ist die
Größenannotation immer korrekt, weil nicht vorhanden.  Bei Knoten ist
eine Größenannotation korrekt, wenn sie die Summe der Größen der
Teilbäume plus 1 (für den Knoten selbst ist).  Außerdem muss die
Funktion auch die Größenannotationen der Teilbäume überprüfen, das
erledigen die rekursiven Aufrufe aus der Schablone.  Fertig sieht das
ganze so aus:
%
\indexvariable{proper-sized-search-tree?}
\begin{lstlisting}
(define proper-sized-search-tree?
  (lambda (search-tree)
    (define proper?
      (lambda (tree)
        (cond
          ((node? tree)
           (define left (node-left-branch tree))
           (define right (node-right-branch tree))
           (and (proper? left)
                (proper? right)
                (= (sized-label-size (node-label tree))
                   (+ 1
                      (sized-tree-size left)
                      (sized-tree-size right)))))
          (else #t))))
    (proper? (sized-search-tree-tree search-tree))))
\end{lstlisting}
% 
Aber geschrieben hatten wir die Funktion, um
\lstinline{balanced-search-tree-insert} zu testen.  Falls die korrekt
ist, dann produziert sie nur Bäume, bei denen
\lstinline{proper-sized-search-tree?} als Ergebnis \lstinline{#t}
liefert.  Wir könnten versucht sein, so etwas hier zu schreiben:

\begin{lstlisting}
(check-property
  (for-all ((search-tree (sized-search-tree-of natural))
            (element natural))
    (proper-sized-search-tree?
      (balanced-search-tree-insert element search-tree))))
\end{lstlisting}
%
Das funktioniert aber nicht, weil die Signatur
\lstinline{(sized-search-tree-of natural)} nicht dafür geeignet ist,
Suchbäume zu generieren.  Insbesondere steht in der
Signatur nur, dass die Größenannotation eine natürliche Zahl ist, aber
nicht welche: Bei den meisten so generierten Suchbäumen wäre sie
falsch.  Und wenn die Eingabe für
\lstinline{balanced-search-tree-insert} schon falsch ist, können wir
nicht erwarten, dass die Ausgabe korrekt ist: Garbage in, Garbage out.

\begin{aufgabeinline}
  Noch andere Aspekte der Signatur
  \lstinline{(sized-search-tree-of natural)}
  machen sie ungeeignet, korrekte Suchbäume zu generieren.  Finde
  einen!
\end{aufgabeinline}
%
Stattdessen rufen wir \lstinline{balanced-search-tree-insert} wiederholt auf,
um korrekte größenannotatierte Suchbäume zu erzeugen.
Die Elemente dafür holen wir aus einer Liste und schreiben
entsprechend eine Funktion, die aus einer Liste einen Suchbaum macht:
%
\begin{lstlisting}
; Aus allen Elementen einer Liste einen Suchbaum machen
(: list->balanced-search-tree ((%a %a -> boolean) (%a %a -> boolean) 
                               (list-of %a)
                               -> (sized-search-tree-of %a)))
\end{lstlisting}
%
Das ist eine typische Aufgabe für \lstinline{fold}: Mit einem leeren
Suchbaum anfangen (für dessen Konstruktion wir die Funktionen für den
Vergleich der Markierungen brauchen) und dann für jedes Listenelement
\lstinline{balanced-search-tree-insert} aufrufen:
%
\indexvariable{list->balanced-search-tree}
\begin{lstlisting}
(define list->balanced-search-tree
  (lambda (label=? label<? elements)
    (fold (make-empty-sized-search-tree label=? label<?)
          balanced-search-tree-insert
          elements)))
\end{lstlisting}
%
Und mit Hilfe dieser Funktion können wir endlich den Test schreiben,
der sicherstellt, dass die Funktion \lstinline{balanced-search-tree-insert} die
Größenannotation richtig macht:
%
\begin{lstlisting}
(check-property
 (for-all ((elements (list-of natural)))
   (proper-sized-search-tree?
    (list->balanced-search-tree = < elements))))
\end{lstlisting}
%
\begin{aufgabeinline}
  Schreibe eine Funktion analog zu
  \lstinline{proper-sized-search-tree?}, die feststellt, ob ein
  Suchbaum auch wirklich sortiert ist und mache daraus eine
  Eigenschaft und einen \lstinline{check-property}-Testfall für
  \lstinline{balanced-search-tree-insert}!
\end{aufgabeinline}
%
Aus der Liste vom Anfang dieses Abschnitts haben wir zwei Punkte
abgehakt. Einer fehlt noch, nämlich zu testen, ob
\lstinline{balanced-search-tree-insert} auch wirklich Bäume liefert,
die balanciert
sind, wie es der Name suggeriert.

Nehmen wir an, \lstinline{balanced-search-tree-insert} würde
\emph{nicht} korrekt balancieren.  Das wäre ziemlich tückisch, weil
die Tests nur die Suchbaumeigenschaft testen, nicht aber die
Balanciertheit.
Erst, wenn Programme es mit größeren Datenmengen zu tun bekommt, gibt es Probleme,
weil die Laufzeit beim Suchen im Baum größer ist als erwartet.

Was heißt eigentlich \emph{genau} balanciert?  Die Funktion
\lstinline{balanced-search-tree-insert} benutzt dafür ja ein
"<weiches"> Kriterium, um nicht jedesmal mit viel Aufwand alles
aufzuräumen.  Wie oft die Funktion neu balanciert, wird durch die
Definition von \lstinline{ratio} auf Seite~\pageref{def:ratio}
kontrolliert.  Stephen Adams, der Autor des zugrundeliegenden Papers,
behauptet, dass bei die Suchbäume immer so ausbalanciert sind, dass
für einen Knoten, dessen linker Teilbaum die Größe $l$
und dessen rechter Teilbaum die Größe $r$ gilt, folgende Formel gilt:
%
\begin{displaymath}
  \frac{l}{\mathtt{ratio}} \leq r \leq l \times \mathtt{ratio}
\end{displaymath}
%
Aus dieser Formel können wir eine Funktion machen, die einen Suchbaum
darauf überprüft, dass sie durch den gesamten Baum hindurch
eingehalten ist.  Das geht nach dem gleichen Muster wie bei
\lstinline{proper-sized-search-tree?}:
%
\indexvariable{balanced-search-tree?}
\begin{lstlisting}
; Ist ein Suchbaum balanciert?
(: balanced-search-tree? ((sized-search-tree-of %a) -> boolean))

(define balanced-search-tree?
  (lambda (search-tree)
    (define balanced?
      (lambda (tree)
        (cond
          ((node? tree)
           (define left (node-left-branch tree))
           (define right (node-right-branch tree)) 
           (define left-size (sized-tree-size left))
           (define right-size (sized-tree-size right))
           (and (balanced? left) (balanced? right)
                (<= (/ left-size ratio)
                    right-size
                    (* left-size ratio))))
          (else #t))))
    (balanced? (sized-search-tree-tree search-tree))))
\end{lstlisting}
%
Ebenfalls nach dem gleichen Muster wie bei
\lstinline{proper-sized-search-tree?} können wir damit eine
Eigenschaft und einen \lstinline{check-property}-Testfall formulieren:
%
\begin{lstlisting}
(check-property
 (for-all ((elements (list-of natural)))
   (balanced-search-tree?
    (list->balanced-search-tree = < elements))))
\end{lstlisting}
%
(Inzwischen kommen soviele Tests zusammen, dass es eine Weile
dauert, bis sie alle durchlaufen.)

Aber hoppla, der Testfall schlägt fehlt.  Bei uns hat er folgendes
Gegenbeispiel produziert:
%
\begin{alltt}
Eigenschaft falsifizierbar mit elements = \framebox{#<list 1 1 3>}
\end{alltt}
%
Wir probieren mal in der REPL aus, was für ein Suchbaum bei dieser
Liste herauskommt:
%
\begin{lstlisting}
(list->balanced-search-tree = < (list 1 1 3))
|\evalsto| #<record:sized-search-tree-of #<function:=> #<function:<> 
     #<record:node-of #<record:sized-label-of 2 3>
                      #<record:node-of #<record:sized-label-of 1 1> 
                                       #f
                                       #f>
                      #f>>
\end{lstlisting}
%
(Die zweite $1$ hätte sich \lstinline{check-property} auch sparen
können.  Offenbar ist es nicht ganz optimal programmiert.)

Was ist passiert?  Grafisch dargestellt sieht der Baum aus der REPL so
aus:
%
\begin{center}
\begin{tikzpicture}
\node (a){$3$}
    child {node (b) {$1$}
      child {node {$\bullet$}} 
      child {node {$\bullet$}}
    }
    child {node {$\bullet$}};
\end{tikzpicture}
\end{center}
%
Und in der Tat: Dieser Baum verletzt die Gleichung
\[\frac{l}{\mathtt{ratio}} \leq r \leq l \times \mathtt{ratio}.\]
In diesem Fall ist $l=1$ und $r=0$.  So richtig schlimm unbalanciert
ist das allerdings gar nicht.  Außerdem ist es gar nicht möglich, die
Gleichung bei einem Suchbaum mit den Elementen 1 und 3 zu erfüllen.
Die einzige andere Möglichkeit ist diese hier:

%
\begin{center}
\begin{tikzpicture}
\node (a){$1$}
    child {node {$\bullet$}}
    child {node (b) {$3$}
      child {node {$\bullet$}} 
      child {node {$\bullet$}}
    };
\end{tikzpicture}
\end{center}
%
Hier gilt $l=0$ und $r=1$ und die Gleichung gilt ebenfalls nicht.
Dass die Gleichung nicht erfüllbar ist, liegt daran, dass der Baum
sehr klein ist: Nur zwei Elemente.

Dieser Umstand ist in der Programmierung von
\lstinline{balanced-search-tree-insert} berücksichtigt.  Schau Dir
nochmal \lstinline{make-balanced-node} auf
Seite~\pageref{func:make-balanced-node} an.  Zur Erinnerung:
%
\indexvariable{make-balanced-node}
\begin{lstlisting}
(define make-balanced-node
  (lambda (label left-branch right-branch)
    (define left-size (sized-tree-size left-branch))
    (define right-size (sized-tree-size right-branch))
    (cond
      ((< (+ left-size right-size) 2)
       (make-sized-node label left-branch right-branch))
      ...)))
\end{lstlisting}
%
Der erste Zweig des \lstinline{cond} schlägt genau dann zu, wenn der
Baum sehr klein ist: Dann wird nicht rotiert oder anderweitig
balanciert.  Das ist bei uns gerade der Fall.  Bei allen größeren
Bäumen greift die Gleichung.  Das ist also etwas schlampig formuliert
in dem Paper, das der Funktion zugrundeliegt, und wir müssen es im
Testfall berücksichtigen, indem wir
%
\begin{lstlisting}
                (<= (/ left-size ratio)
                    right-size
                    (* left-size ratio)))))
\end{lstlisting}
%
ersetzen durch:
%
\begin{lstlisting}
                (or (< (+ left-size right-size) 2)
                    (<= (/ left-size ratio)
                        right-size
                        (* left-size ratio)))))
\end{lstlisting}
%
Und siehe da: Jetzt läuft der Testfall durch.
Es kommt immer mal wieder vor, dass ein
Testfall mit \lstinline{check-property} Gegenbeispiele findet, die
eigentlich keine sind, weil wir die Bedingung für den Test nicht ganz
richtig formuliert haben.  Den eigentlichen Fehler zu finden, nervt
oft, aber manchmal erfahren wir auch etwas bei der Gelegenheit, was
wir noch nicht gewusst haben.  (In diesem Fall: Dass kleine Bäume
gesondert behandelt werden müssen.)
%
\begin{aufgabeinline}
  Was passiert, wenn Du den Zweig für kleine Bäume aus
  \lstinline{make-balanced-node} entfernst?  Findet das einer der
  Teställe heraus?  Was genau ist die Ursache des angezeigten Fehlers?
\end{aufgabeinline}
%
Die Liste vom Anfang des Abschnitts haben wir damit abgearbeitet.
Haben wir mit den bisherigen Tests ausreichend sichergestellt, dass
\lstinline{balanced-search-tree-insert} korrekt funktioniert?
Nun, wir haben überprüft, dass die entstehenden Suchbäume die korrekte
Form haben.  Allerdings haben wir noch gar nicht überprüft, dass auch
der Inhalt stimmt.  Dazu benutzen wir den zweiten Hinweis aus
Abschnitt~\ref{sec:ka-testfaelle} auf
Seite~\pageref{sec:ka-testfaelle}:
%
\begin{quote}
  Oft gehören zu einem Problem mehrere Funktionen, die auf bestimmte
  Art und \mbox{Weise} zusammenarbeiten.  Schreibe auf, wie diese
  Zusammenarbeit aussieht.
\end{quote}
%
Die Funktion \lstinline{balanced-search-tree-insert} ist ja nur
insofern sinnvoll, dass die damit eingefügten Elemente mit
\lstinline{sized-search-tree-member?} auch gefunden werden können. Das
ist gerade das gefragte Zusammenspiel mehrerer Funktionen.  Zu diesem
Zweck benutzen wir wieder \lstinline{list->balanced-search-tree}, um
aus einer Liste einen Suchbaum herzustellen und überprüfen, dass
\lstinline{sized-search-tree-member?} auch für jedes Element der Liste
\lstinline{#t} liefert:
%
\begin{lstlisting}
(check-property
 (for-all ((elements (list-of natural)))
   (define search-tree (list->balanced-search-tree = < elements))
   (every? (lambda (element)
             (sized-search-tree-member? element search-tree))
           elements)))
\end{lstlisting}
%
Die Funktion \lstinline{every?} haben wir extra für diesen Testfall
programmiert:\label{func:everyp}
%
\indexvariable{every?}
\begin{lstlisting}
; Liefert eine Funktion für alle Elemente einer Liste #t?
(: every? ((%a -> boolean) (list-of %a) -> boolean))

(check-expect (every? even? (list 2 4 6)) #t)
(check-expect (every? positive? (list 1 2 3)) #t)
(check-expect (every? positive? (list 1 0 3)) #f)

(define every?
  (lambda (p? list)
    (cond
      ((empty? list) #t)
      ((cons? list)
       (and (p? (first list))
            (every? p? (rest list)))))))
\end{lstlisting}
%
Das ist schon mal gut, aber Du erinnerst Dich an den dritten Hinweis in
Abschnitt~\ref{sec:ka-testfaelle} auf
Seite~\pageref{sec:ka-testfaelle}?
%
\begin{quote}
  Versuche, die bestehenden Eigenschaften durch einfache aber
  fehlerhafte Varianten Deiner Funktion auszutricksen.
\end{quote}
%
\begin{aufgabeinline}
  Finde eine einfache, aber fehlerhafte Variante der Funktion
  \lstinline{balanced-search-tree-insert}, die alle bisherigen
  Testfälle austrickst!
\end{aufgabeinline}
%
Wir benötigen also auf jeden Fall noch eine Funktion, die überprüft,
dass Werte, die \emph{nicht} in einem Suchbaum stehen, auch
tatsächlich \emph{nicht} gefunden werden.  Wir fangen so an wie bisher:
%
\begin{lstlisting}
(check-property
 (for-all ((elements (list-of natural)))
   ...
   (list->balanced-search-tree = < elements)
   ...))
\end{lstlisting}
%
Wir brauchen jetzt noch irgendeine Zahl, die wir darauf überprüfen
können, dass sie nicht im Suchbaum ist.  Die holt sich der Testfall
auch mit \lstinline{for-all}:
%
\begin{lstlisting}
(check-property
 (for-all ((elements (list-of natural))
           (number natural))
   ...
   (not (sized-search-tree-member?
           number
           (list->balanced-search-tree = < elements)))
   ...))
\end{lstlisting}
%
Um sicherzustellen, dass
\lstinline{number} nicht zufällig doch im Suchbaum ist, benutzen
wir \lstinline{==>}:
%
\begin{lstlisting}
(check-property
 (for-all ((elements (list-of natural))
           (number natural))
   (==> (not (member? = number elements))
        (not (sized-search-tree-member?
              number
              (list->balanced-search-tree = < elements))))))
\end{lstlisting}
%
Da steht also umgangssprachlich formuliert:

Für alle Listen von
Elementen \lstinline{elements} und jede Zahl \lstinline{number} gilt:
Wenn \lstinline{number} nicht zu \lstinline{elements} gehört, dann
liefert \lstinline{sized-search-tree-member?} für \lstinline{number}
und den Suchbaum aus den Zahlen in \lstinline{elements} das Ergebnis
\lstinline{#f}.
Mit dieser Eigenschaft haben wir das Zusammenspiel zwischen
\lstinline{balanced-search-tree-insert} und
\lstinline{sized-search-tree-member?} ausreichend beschrieben und
können ziemlich ruhig schlafen in der Gewissheit, dass die Funktionen
korrekt arbeiten.

\section{Algebraische Eigenschaften}
\label{sec:algebraische-eigenschaften}

Hast Du das hier schonmal gesehen?
%
\begin{displaymath}
  (a + b) + c = a + (b + c)
\end{displaymath}
%
Oder das hier?
%
\begin{displaymath}
  (a \times b) \times c = a \times (b \times c)
\end{displaymath}
%
Diese Gleichungen sind unter dem Namen
\textit{Assoziativität}\index{Assoziativität} bekannt, manchmal auch
als \textit{Assoziativgesetz}.  Kurz kam das Wort schonmal auf
Seite~\pageref{page:assoziativitaet} vor, und da steht folgende Gleichung:
%
\begin{displaymath}
  {\rm cat}(u,{\rm cat}(v,w))  = {\rm cat}({\rm cat}(u,v),w).
\end{displaymath}
%
Die Assoziativität ist eine äußerst nützliche Gleichung, weil sie
aussagt, dass in einer Aneinanderreihung von $+$ oder $\times$ jeweils
die Klammern vollkommen egal sind: Und wenn sie schon egal sind, kann
man sie auch weglassen.

Die Assoziativität ist nicht einfach eine Gleichung (hier sind es ja
schon drei), sondern eine Eigenschaft
der Funktionen $+$ und
$\times$ und cat.  Entsprechend kann man sagen "<$+$ ist
assoziativ"> oder "<cat ist assoziativ">.  Alle diese Funktionen haben die Struktur
ihrer Signaturen gemeinsam.  Hier sind diese Signaturen, so als wenn sie in
einem Programm stünden:
%
\begin{lstlisting}
(: + (number number -> number))
(: * (number number -> number))
(: concatenate ((list-of %a) (list-of %a) -> (list-of %a)))
\end{lstlisting}
%
(Statt der mathematischen Funktion cat haben wir die Funktion
\lstinline{concatenate} aus Abschnitt~\ref{sec:concatenate} auf
Seite~\pageref{sec:concatenate} aufgeführt.)
%
\begin{aufgabeinline}
  Sind \lstinline{and} und \lstinline{or} assoziativ?  Wie passen ihre
  Signaturen zu denen von den Funktionen oben?
\end{aufgabeinline}
%
Diese Form von Signaturen haben wir schon gesehen, als es um
Kombinatoren ging, in Kapitel~\ref{cha:selbstbezug} auf
Seite~\pageref{cha:selbstbezug}.  Eine assoziative Funktion ist also
eine spezielle Sorte Kombinator.\index{Kombinator}

Assoziative Operationen gibt es so viele, dass es sich lohnt, auf
Verdacht danach zu suchen, wenn Du eine neue Datendefinition
erstellst.  Und wenn Du einen assoziativen Kombinator gefunden hast,
lohnt es sich, diese Erkenntnis aufzuschreiben.  Im Gespräch mit
anderen kannst Du dann einfach sagen "<cat ist assoziativ">, und im
besten Fall wissen alle, was gemeint ist.

Wir können die Assoziativität aber auch als Eigenschaft mit
\lstinline{check-property} aufschreiben.  Wir machen das erstmal mit
\lstinline{concatenate}, \lstinline{+} und \lstinline{*} kommen
danach.
%
\begin{lstlisting}
(check-property
 (for-all ((a (list-of integer))
           (b (list-of integer))
           (c (list-of integer)))
   (expect (concatenate (concatenate a b) c)
           (concatenate a (concatenate b c)))))
\end{lstlisting}
%
Du fragst Dich vielleicht, warum \lstinline{(list-of integer)} als
Signatur und nicht \lstinline{(list-of %a)},
wie es in der Signaturdeklaration von \lstinline{concatenate} steht.
Das liegt daran, dass bei Signaturen in \lstinline{for-all} keine
Signaturvariablen stehen dürfen, damit DrRacket dafür vernünftig
zufällige Werte generieren kann.  (Siehe dazu auch
Abbildung~\ref{scheme:check-property} auf
Seite~\pageref{scheme:check-property}.)

Und dann ist da noch was, nämlich die Funktion \lstinline{expect}: Die
brauchen wir, um die beiden Listen zu vergleichen, die bei
\lstinline{concatenate} herauskommen.  Bisher kennen wir ja nur
Funktionen, die Zahlen vergleichen (\lstinline{=}), Zeichenketten
(\lstinline{string=?}) und Booleans (\lstinline{boolean=?}).  Eine
allgemeine Vergleichsfunktion für Listen gibt es nicht.
\lstinline{Expect} liefert eine Eigenschaft, die beliebige Werte
vergleicht~-- siehe Abbildung~\ref{scheme:expect}.
%
\begin{feature}{\lstinline{expect}}{scheme:expect}
  \lstinline{Expect}\indexvariable{expect} liefert eine
  Eigenschaft analog zur Funktionsweise von
  \lstinline{check-expect}.  Ein \lstinline{expect}-Ausdruck hat folgende
  Form:
  %
\begin{lstlisting}
(expect $e\sb{1}$  $e\sb{2}$)
\end{lstlisting}
%
$e_1$ und $e_2$ sind Ausdrücke.  Die resultierende Eigenschaft ist
erfüllt, wenn $e_1$ und $e_2$ den gleichen Wert liefern~-- der
Vergleich wird dabei wie bei \lstinline{check-expect} angestellt.

Da \lstinline{expect} wie \lstinline{check-expect} vergleicht,
funktioniert es nicht auf inexakten Zahlen.
\end{feature}
%
\begin{aufgabeinline}
  Schreibe mit Hilfe des Teachpacks \texttt{image.rkt} Eigenschaften
  für die Assoziativität der Kombinatoren aus Abschnitt
  \ref{sec:image-combinators} auf Seite \pageref{sec:image-combinators}~--\lstinline{overlay},
  \lstinline{beside} und \lstinline{above}.
\end{aufgabeinline}
%
Eine assoziative Funktion macht aus zwei "<Dingsen"> ein
"<Dings">.  \lstinline{+} macht aus zwei Zahlen eine,
\lstinline{concatenate} aus zwei Listen eine, \lstinline{and} aus zwei
booleschen Werten einen.

Über die Signaturdeklarationen von \lstinline{+}, \lstinline{*},
\lstinline{concatenate} können wir abstrahieren:
%
\begin{lstlisting}
(: $\mathit{op}$ ($s$ $s$ -> $s$))
\end{lstlisting}
%
Zur Assoziativität gehört also neben der Operation $op$ auch die
Signatur $s$, so dass $op$ die Signatur \lstinline{($s$ $s$ -> $s$)}
hat.  (Und natürlich die Assoziativitätsgleichung selbst.)

Solche "<Dreigestirne"> aus "<Grundsignatur">, Operation (oder
mehreren Operationen) und Gleichungen werden in der mathematischen
Algebra\index{Algebra} studiert und klassifiziert.  (Dort wird statt
mit Signaturen mit Mengen hantiert.)  Die besonders nützlichen,
interessanten oder häufig vorkommenden dieser Dreigestirne~--
algebraischer Strukturen~--bekommen eigene Namen.

Eine Kombination aus Signatur, Kominator mit Signatur
\lstinline{($s$ $s$ -> $s$)}
und Assoziativgesetz heißt zum Beispiel
\textit{Halbgruppe}.\index{Halbgruppe}\footnote{Wenn es "<Halbgruppen"> gibt,
gibt es dann auch "<Gruppen">, magst Du fragen.  Gibt es, und in der
Algebra gibt es einen großen Teilbereich namens "<Gruppentheorie">.
Gruppen gibt es in der Programmierung aber viel seltener als
Halbgruppen, darum konzentrieren wir uns auf letztere.}

Viele Halbgruppen erfüllen noch eine weitere Eigenschaft: Sie besitzen
einen Wert der Signatur, der "<nichts macht">, das sogenannte
"<neutrale Element">.\index{neutrales Element} Das hat in
Abschnitt~\ref{page:neutrales-element} auf
Seite~\ref{page:neutrales-element} schonmal eine Rolle gespielt.
Jetzt können wir es endlich richtig einordnen.

Nennen wir das neutrale Element $n$.  Dann gelten folgende
Eigenschaften:
%
\begin{lstlisting}
(for-all ((a $s$))
  (expect ($op$ a $n$) a))
(for-all ((a $s$))
  (expect ($op$ $n$ a) a)))
\end{lstlisting}
%
Falls Du Dich fragst, warum wir nicht einfach \lstinline{and}
benutzen, um beide Eigenschaften zusammenzufassen.  Das liegt daran,
dass \lstinline{and} nur auf Booleans funktioniert, \lstinline{expect}
aber eine Eigenschaft liefert.

Das neutrale Element kann von Halbgruppe zu Halbgruppe varrieren,
selbst wenn die Signatur $s$ immer die Gleiche ist.  Zum Beispiel ist
$0$ das neutrale Element von $+$ und $1$ das neutrale Element von
$\times$, auch wenn es beide Male um Zahlen geht.

\begin{aufgabeinline}
  Was ist das neutrale Element von \lstinline{or} beziehungsweise
  \lstinline{and}?
\end{aufgabeinline}
%
Bei \lstinline{concatenate} ist das neutrale Element die leere Liste.
Das können wir mit \lstinline{check-property} festhalten:
%
\begin{lstlisting}
(check-property
 (for-all ((a (list-of integer)))
   (expect (concatenate a empty) a)))

(check-property
 (for-all ((a (list-of integer)))
   (expect (concatenate empty a) a)))
\end{lstlisting}
%
Auch für \lstinline{overlay}, \lstinline{beside} und \lstinline{above}
gibt es ein neutrales Element.  Es heißt
\lstinline{empty-image}\indexvariable{empty-image}.
%
\begin{aufgabeinline}
  Formuliere \lstinline{check-property}-Testfälle, die zeigen dass
  \lstinline{empty-image} ein neutrales Element bezüglich
  \lstinline{overlay}, \lstinline{beside} und \lstinline{above} ist.
\end{aufgabeinline}
%
Wie Du siehst, haben alle Halbgruppen, die wir bisher betrachtet
haben, ein neutrales Element.  In der Tat ist das meistens so.  Sogar
so oft, dass, wenn bei Deiner Datenanalyse eine Halbgruppe
herausgekommen ist, Du immer auch nach einem neutralen Element
Ausschau halten solltest.  Eine Halbgruppe mit einem neutralen Element
hat entsprechend auch einen Namen, nämlich \textit{Monoid}.\index{Monoid}

Falls Dir die Assoziativität schon früher bekannt war, dann
wahrscheinlich im Zusammenhang mit Zahlen.  Die können wir natürlich
auch mit \lstinline{check-property} zum Ausdruck bringen:
%
\begin{lstlisting}
(check-property
 (for-all ((a number)
           (b number)
           (c number))
    (= (+ a (+ b c))
       (+ (+ a b) c))))
\end{lstlisting}
%
Dabei gibt es aber eine Überraschung:
%
\begin{alltt}
Eigenschaft falsifizierbar mit
  a = \framebox{#i9.75} b = \framebox{-9} c = \framebox{#i-7.7}
\end{alltt}
%
(Die genauen Zahlen lauten bei Dir vielleicht anders.)

Und Tatsache, wenn wir das in der REPL ausprobieren, kommt bei den
beiden Seiten der Gleichheit etwas unterschiedliches heraus:
%
\begin{lstlisting}
(+ #i9.75 (+ -9 #i-7.7))
|\evalsto| #i-6.949999999999999
(+ (+ #i9.75 -9) #i-7.7)
|\evalsto| #i-6.95
\end{lstlisting}
%
Du erinnerst Dich an Abschnitt~\ref{sec:inexakt} auf
Seite~\ref{sec:inexakt}: Das \lstinline{#i} steht für "<inexakt">, was
bedeutet, dass die Addition bei diesen Zahlen rundet.  Leider macht
das Runden auch die Assoziativität kaputt.  Es wird besser, wenn wir
\lstinline{number} durch \lstinline{rational} ersetzen, denn beim
Rechnen mit rationalen Zahlen wird nicht gerundet.

Vorsicht also beim Verwenden von reellen Zahlen in Eigenschaften, also
der Signaturen \lstinline{real} und \lstinline{number}.  Im
Zweifelsfall lieber \lstinline{rational} benutzen!

\section{Eigenschaften von Funktionen auf Listen}

Listen bilden ja mit \lstinline{concatenate} eine Halbgruppe, was
\lstinline{concatenate} eine besondere Bedeutung als Listenoperation
zukommen lässt.  Die können wir ausspielen, wenn wir Tests auf
Listenfunktionen formulieren wollen, indem wir sie im Zusammenhang mit
\lstinline{concatenate} bringen.

Zur Erinnerung, die \lstinline{list-sum}-Funktion hat folgende
Signatur:
%
\begin{lstlisting}
(: list-sum ((list-of number) -> number))
\end{lstlisting}
%
Da die Funktion eine Liste als Eingabe hat, können wir untersuchen,
was passiert, wenn die Liste durch \lstinline{concatenate} entsteht:
%
\begin{lstlisting}
(check-property
 (for-all ((a (list-of rational))
           (b (list-of rational)))
   (= (list-sum (concatenate a b))
      (+ (list-sum a) (list-sum b)))))
\end{lstlisting}
%
Dran denken: Bei \lstinline{for-all} nicht \lstinline{number},
sondern \lstinline{rational} benutzen, um Problemen mit der Rundung
aus dem Weg zu gehen.

Was passiert hier?  Der Aufruf von \lstinline{list-sum} wird von der
linken auf die rechte Seite der Gleichung "<nach innen"> gedrückt.
Außerdem wird aus dem \lstinline{concatenate} auf Listen auf der
linken Seite der Gleichung die Addition zweier Zahlen auf der rechten
Seite.

Nun bilden Listen mit \lstinline{concatenate} eine Halbgruppe, genauso
wie Zahlen mit \lstinline{+}. Die Funktion \lstinline{list-sum} bildet
nicht nur Listen auf Zahlen ab, sondern macht auch aus
\lstinline{concatenate} bei den Listen die Summe bei den Zahlen:
Die Struktur der einen Halbgruppe wird mit \lstinline{list-sum} in die
Struktur der anderen Halbgruppe abgebildet.  Eine solche Funktion heißt in
der Algebra \textit{Homomorphismus}.\index{Homomorphismus} Wenn man
den Begriff verwendet, sollte man immer dazusagen, auf welche
algebraische Struktur er sich bezieht.  Hier handelt es sich um einen
\textit{Halbgruppen"=Homomorphismus}.  Wenn Du einen Homomorphismus in
Deinem Code findest, ist das fast immer ein gutes Zeichen~-- Du bist
wahrscheinlich einer nützlichen Einsicht auf der Spur.
%
\begin{aufgabeinline}
  Zeige, dass \lstinline{list-sum} sogar ein Monoiden-Homomorphismus
  ist, also aus dem neutralen Element in dem einen Monoiden das
  neutrale Element in dem anderen Monoiden wird.  Schreibe dazu einen
  \lstinline{check-property}-Testfall!
\end{aufgabeinline}

\begin{aufgabeinline}
  Formuliere eine Eigenschaft von \lstinline{invert} mit Hilfe von
  \lstinline{concatenate} und schreibe dazu einen
  \lstinline{check-property}-Testfall!
\end{aufgabeinline}

\section{Exkurs: Eigenschaften beweisen}
\label{sec:eigenschaften-beweisen}

\lstinline{Check-property} ist ziemlich gut darin, Gegenbeispiele zu
finden für Eigenschaften, die nicht gelten.  Aber würden wir
\lstinline{check-property}~-- sagen wir mal~-- zutrauen, die
Korrektheit der Steuersoftware für ein Flugzeug sicherzustellen?  
Immerhin ist es möglich, dass bei den 100~Tests, die
\lstinline{check-property} zufällig generiert, das eine Gegenbeispiel
einfach nicht dabei ist.  

Wenn also eine Eigenschaft wirklich unverzichtbar für den Einsatz
einer Software ist, sollten wir die Sicherheit, dass kritische
Eigenschaften gelten, noch weiter erhöhen.  Das geht zum Beispiel,
indem wir mathematisch \emph{beweisen}, dass eine Eigenschaft gilt.
Wie das gehen kann, zeigt dieser Abschnitt exemplarisch.  

Wie wir sehen werden, ist das ganz schön mühsam: Wir haben ja schon
Eigenschaften von Funktionen in Kapitel~\ref{cha:indu} bewiesen, zum
Beispiel die Assoziativität von cat in
Abschnitt~\ref{sec:sequence-induction} auf
Seite~\pageref{sec:sequence-induction}.  Wir nehmen uns hier noch
einmal die Assoziativität vor, allerdings diesmal nicht auf der
mathematischen cat, sondern der programmierten Funktion
\lstinline{concatenate}.  

Wir wollen also folgendes beweisen: Für alle Listen $u$, $v$ und $w$ gilt:
%
\begin{lstlisting}
(expect (concatenate $u$ (concatenate $v$ $w$))
        (concatenate (concatenate $u$ $v$) $w$))
\end{lstlisting}
%
Grundsätzlich führen wir den Beweis wie bei der mathematischen
Funktion cat auch über Induktion.  Anders als dort können wir bei
\lstinline{concatenate} aber nicht einfach beliebig Gleichungen
einsetzen.  Wir müssen stattdessen bewesen, dass DrRacket bei der
Auswertung für beide Seiten der \lstinline{expect}-"<Gleichung"> das
gleiche Ergebnis berechnet.  Dabei müssen wir berücksichtigen, dass
DrRacket die Auswertungsschritte für einen Aufruf von
\lstinline{concatenate} in einer bestimmten Reihenfolge durchführt.
Wir müssen also beim Beweis so vorgehen, wie es der Stepper tun würde.
Eigentlich müssten wir diese Auswertungsstrategie sogar noch
formalisieren, um wirklich einen Beweis zu führen.  Das machen wir im
späteren Kapitel~\ref{chap:lambda} auf Seite~\pageref{chap:lambda}.
Hier begnügen wir uns mit der Einsicht, dass bei einem Funktionsaufruf
die Argumente ausgewertet werden, bevor es mit der Auswertung des
Funktionsrumpfes weitergeht.

Wir benutzen eine Induktionsschablone wie in
Abschnitt~\ref{sec:sequence-induction} auf
Seite~\pageref{sec:sequence-induction}.
%
\begin{enumerate}
\item Wir entscheiden uns genau wie dort für eine Induktion über $u$.
  Damit die Schablone passt, benutzen wir dafür den Namen $f$,
  formulieren also die Eigenschaft so um:
%
\begin{lstlisting}
(expect (concatenate $f$ (concatenate $v$ $w$))
        (concatenate (concatenate $f$ $v$) $w$))
\end{lstlisting}
%
\item Als nächstes betrachten wir den Fall, dass $f$ die leere Liste
  \lstinline{#<empty-list>} ist.  Die Gleichung sieht dann so aus:
\begin{lstlisting}
(expect (concatenate #<empty-list> (concatenate $v$ $w$))
        (concatenate (concatenate #<empty-list> $v$) $w$))
\end{lstlisting}
\item Diese Gleichung beweisen wir nun, angefangen mit der "<linken
  Seite"> der Gleichung.  DrRacket würde bei der Auswertung zunächst
  das erste \lstinline{concatenate} auswerten, also durch seine
  Definition ersetzen sowie \lstinline{empty} zu
  \lstinline{#<empty-list>} auswerten:
\begin{lstlisting}
(concatenate #<empty-list> (concatenate $v$ $w$))
|\evalsto{}| (($\lambda$ (list1 list2) ...) #<empty-list> (concatenate $v$ $w$))
\end{lstlisting}
%
(Wir haben $\lambda$ statt \lstinline{lambda} geschrieben um Platz zu
sparen.)

Als nächstes wird \lstinline{(concatenate $v$ $w$)} ausgwertet. Da wir
gar nicht wissen, was $v$ und $w$ sind, wissen wir weder, was da
herauskommt, noch, wie viele Schritte das benötigt.  Irgendwas wird
aber herauskommen~-- wir nennen das $vw$:
%
\begin{lstlisting}
|\evalsto{} $\ldots$ \evalsto{}| (($\lambda$ (list1 list2) ...) #<empty-list> $vw$)
\end{lstlisting}
%
Jetzt können wir endlich mit dem Rumpf der Funktion weitermachen.  Wir
setzen für \lstinline{list1} \lstinline{#<empty-list>} ein, für
\lstinline{list2} $vw$:
%
\begin{lstlisting}
|\evalsto{}| (cond ((empty? #<empty-list>) $vw$) ((cons? #<empty-list>) ...))
\end{lstlisting}
Beim \lstinline{cond} greift sofort der erste Zweig:
\begin{lstlisting}
|\evalsto{}| (cond (#t $vw$) ((cons? #<empty-list>) ...))
|\evalsto{}| $vw$
\end{lstlisting}
%
Weiter geht's hier nicht.  Wir nehmen uns deshalb die andere Seite der
Gleichung vor:

\begin{lstlisting}
(concatenate (concatenate $f$ $v$) $w$)
$=$ (concatenate (concatenate #<empty-list> $v$) $w$)
\end{lstlisting}
%
Auch hier wird DrRacket für die beiden \lstinline{concatenate} jeweils
die Definition einsetzen:
%
\begin{lstlisting}
|\evalsto{}| (($\lambda$ (list1 list2) ...) (concatenate #<empty-list> $v$) $w$) 
|\evalsto{}| (($\lambda$ (list1 list2) ...) 
      (($\lambda$ (list1 list2) ...) #<empty-list> $v$) $w$)
\end{lstlisting}
%
Hier wird der "<innere"> Aufruf von \lstinline{concatenate} zuerst ausgewertet:
%
\begin{lstlisting}
|\evalsto{}| (($\lambda$ (list1 list2) ...)
      (cond ((empty? #<empty-list>) $v$) 
            ((cons? #<empty-list>) ...)) $w$) 
|\evalsto{}| (($\lambda$ (list1 list2) ...) $v$ $w$)
|\evalsto{} \ldots{} \evalsto{}| $vw$
\end{lstlisting}
%
Es kommt also dasselbe heraus wie bei der linken Seite der Gleichung.
Für die leere Liste ist die Eigenschaft also bewiesen.

\item Als nächstes müssen wir die Induktionsvoraussetzung
  formulieren.  Die sieht so aus:
\begin{lstlisting}
(expect (concatenate $f$ (concatenate $v$ $w$))
        (concatenate (concatenate $f$ $v$) $w$))
\end{lstlisting}

\item Es folgt der Induktionsschluss.  Dafür müssen wir eine Liste
  betrachten, die um "<eins länger"> ist als $f$, also aus einem
  ersten Element $f_1$ und Rest $f$ besteht.  Wir nennen diese Liste
  $f_1f$:
  %
\begin{lstlisting}
(expect (concatenate $f_1f$ (concatenate $v$ $w$))
        (concatenate (concatenate $f_1f$ $v$) $w$))
\end{lstlisting}
  %
\item Um den Induktionsschluss zu beweisen, werten wir zunächst die
  linke Seite aus.  Wir benutzen wieder den Namen $vw$ für das
  Ergebnis von \lstinline{(concatenate $v$ $w$)}:
  % 
\begin{lstlisting}
(concatenate $f_1f$ (concatenate $v$ $w$))
|\evalsto{}| (($\lambda$ (list1 list2) ...) $f1_f$ (concatenate $v$ $w$))
|\evalsto{} $\ldots$ \evalsto{}| (($\lambda$ (list1 list2) ...) $f_1f$ $vw$)
|\evalsto{}| (cond ((empty? $f_1f$) $vw$)
          ((cons? $f_1f$) 
           (cons (first $f_1f$) (concatenate (rest $f_1f$) $vw$))))
\end{lstlisting}
  Diesmal ist der \lstinline{cons?}-Zweig dran, weil $f_1f$ nicht leer ist:
  %
\begin{lstlisting}
|\evalsto{}| (cond (#f $vw$)
         ((cons? $f_1f$)
          (cons (first $f_1f$) (concatenate (rest $f_1f$) $vw$))))
|\evalsto{}| (cond ((cons? $f_1f$)
          (cons (first $f_1f$) (concatenate (rest $f_1f$) $vw$))))
|\evalsto{}| (cond (#t (cons (first $f_1f$) (concatenate (rest $f_1f$) $vw$))))
|\evalsto{}| (cons (first $f_1f$) (concatenate (rest $f_1f$) $vw$))
|\evalsto{}| (cons $f_1$ (concatenate (rest $f_1f$) $vw$))
|\evalsto{}| (cons $f_1$ (concatenate (rest $f_1f$) $vw$))
|\evalsto{}| (cons $f_1$ (($\lambda$ (list1 list2) ...) (rest $f_1f$) $vw$))
|\evalsto{}| (cons $f_1$ (($\lambda$ (list1 list2) ...) $f$ $vw$))
\end{lstlisting}
  %
  Weiter geht es nicht.  Wir nehmen uns darum die rechte Seite vor:
  %
\begin{lstlisting}
(concatenate (concatenate $f_1f$ $v$) $w$)
|\evalsto{}| (($\lambda$ (list1 list2) ...) (concatenate $f_1f$ $v$) $w$)
|\evalsto{}| (($\lambda$ (list1 list2) ...) (($\lambda$ (list1 list2) ...) $f_1f$ $v$) $w$)
|\evalsto{}| (($\lambda$ (list1 list2) ...)
     (cond ((empty? $f_1f$) $v$) 
           ((cons? $f_1f$) (cons (first $f_1f$)
                              (concatenate (rest $f_1f$) $v$)))) $w$)
|\evalsto{}| (($\lambda$ (list1 list2) ...)
     (cond (#f $v$) 
           ((cons? $f_1f$) (cons (first $f_1f$)
                              (concatenate (rest $f_1f$) $v$)))) $w$)
|\evalsto{}| (($\lambda$ (list1 list2) ...)
     (cond ((cons? $f_1f$) (cons (first $f_1f$)
                              (concatenate (rest $f_1f$) $v$)))) $w$)
|\evalsto{}| (($\lambda$ (list1 list2) ...)
     (cond (#t (cons (first $f_1f$) (concatenate (rest $f_1f$) $v$)))) $w$)
|\evalsto{}| (($\lambda$ (list1 list2) ...) 
     (cons (first $f_1f$) (concatenate (rest $f_1f$) $v$)) $w$)
|\evalsto{}| (($\lambda$ (list1 list2) ...) (cons $f_1$ (concatenate (rest $f_1f$) $v$)) $w$)
|\evalsto{}| (($\lambda$ (list1 list2) ...)
     (cons $f_1$ (($\lambda$ (list1 list2) ...) (rest $f_1f$) $v$)) $w$)
|\evalsto{}| (($\lambda$ (list1 list2) ...) (cons $f_1$ (($\lambda$ (list1 list2) ...) $f$ $v$)) $w$)
\end{lstlisting}
  %
  Wir wissen nicht, was $f$, $v$
  und $w$ sind.  Wir nehmen aber an, dass bei der
  Auswertung von \lstinline{(($\lambda$ (list1 list2) ...) $f$ $v$)}
  \emph{irgendetwas} herauskommt und nennen das $fv$:
  %
\begin{lstlisting}
|\evalsto{} $\ldots$ \evalsto{}| (($\lambda$ (list1 list2) ...) (cons $f_1$ $fv$) $w$)
\end{lstlisting}
  %
  Dem Ergebnis von \lstinline{(cons $f_1$ $fv$)} können wir ebenfalls
  einen Namen geben, wir nehmen wenig einfallsreich $f_1fv$.  Da diese
  Liste ein erstes Element $f_1$ hat, ist sie nicht leer:
%
\begin{lstlisting}
|\evalsto{}| (($\lambda$ (list1 list2) ...) $f_1fv$ $w$)
|\evalsto{}| (cond ((empty? $f_1fv$) ...) 
         ((cons? $f_1fv$)
          (cons (first $f_1fv$) (concatenate (rest $f_1fv$) $w$))))
|\evalsto{}| (cond (#f ...) 
         ((cons? $f_1fv$)
          (cons (first $f_1fv$) (concatenate (rest $f_1fv$) $w$))))
|\evalsto{}| (cond ((cons? $f_1fv$)
          (cons (first $f_1fv$) (concatenate (rest $f_1fv$) $w$))))
|\evalsto{}| (cond (#t (cons (first $f_1fv$) (concatenate (rest $f_1fv$) $w$))))
|\evalsto{}| (cons (first $f_1fv$) (concatenate (rest $f_1fv$) $w$))
|\evalsto{}| (cons $f_1$ (concatenate (rest $f_1fv$) $w$))
|\evalsto{}| (cons $f_1$ (($\lambda$ (list1 list2) ...) (rest $f_1fv$) $w$))
|\evalsto{}| (cons $f_1$ (($\lambda$ (list1 list2) ...) $fv$ $w$))
\end{lstlisting}
\end{enumerate}
%
Jetzt geht es aber wirklich nicht mehr weiter.  Wir können das mit
dem Ergebnis der linken Seite vergleichen, die immerhin auch mit
\lstinline{(cons $f_1$ ...)} anfängt.  Ansonsten steht da links:
% 
\begin{lstlisting}
(($\lambda$ (list1 list2) ...) $f$ $vw$)
\end{lstlisting}
% 
\ldots{} und rechts:
\begin{lstlisting}
((lambda (list1 list2) ...) $fv$ $w$)
\end{lstlisting}
%
Um zu beweisen, dass diese beiden Ausdrücke das gleiche liefern,
ziehen wir die Induktionsvoraussetzung hinzu.  Hier ist sie zur
Erinnerung:
\begin{lstlisting}
(expect (concatenate $f$ (concatenate $v$ $w$))
        (concatenate (concatenate $f$ $v$) $w$))
\end{lstlisting}
% 
Wir hatten den Namen $vw$ für das Ergebnis von
\lstinline{(concatenate $v$ $w$)} und den Namen $fv$ für das
Ergebnis von \lstinline{(concatenate $f$ $v$)}.  Außerdem steht
\lstinline{($\lambda$ (list1 list2) ...)} ja für
\lstinline{concatenate}.  Wenn wir das in die
Induktionsvoraussetzung einsetzen, steht da genau das, was wir
brauchen, nämlich dass linke und rechte Seite das gleiche Ergebnis haben.
Geschafft!

Aber das ist schon ziemlich viel Arbeit, und auch
fehleranfällig.  In der Praxis funktioniert das nur für kleine
Funktionen.  Wer Eigenschaften größerer Programme beweisen möchte,
benutzt dafür in der Regel spezielle Werkzeuge, welche die Beweise
überprüfen und in weiten Teilen auch automatisch herleiten können.

\section*{Aufgaben}

\begin{aufgabe}
Welche interessanten Eigenschaften hat die Division?  Schreibe
diese als Eigenschaften von \lstinline{/} auf.
\end{aufgabe}

\begin{aufgabe}
  Schreibe eine möglichst vollständige Liste interessanter
  Eigenschaften der Dir bekannten arithmetischen 
  und logischen Operationen auf.  Beziehe dazu auch die
  Vergleichsoperationen $<$, $\leq$ etc.\ ein.  Finde außerdem
  für jede Operation eine interessante Eigenschaft, die \emph{nicht}
  gilt und überprüfe, ob \drscheme{} jeweils ein Gegenbeispiel
  findet.
\end{aufgabe}

\begin{aufgabe}
  \label{aufgabe:boolean-distrib}
  Für Multiplikation und Addition gilt das
  \textit{Distibutivgesetz}\index{Distributivität}:
  %
  \begin{displaymath}
    a\cdot(b + c) = a\cdot b + a \cdot c
  \end{displaymath}
  %
  Auch dieses Gesetz ist nicht auf Zahlen beschränkt.  Für
  \lstinline{and} und \lstinline{or} gilt es ebenfalls.  Formuliere
  dieses als Eigenschaften und lasse sie \drscheme{} sie überprüfen.
\end{aufgabe}

\begin{aufgabe}
  Formuliere Eigenschaften von \lstinline{filter} und \lstinline{map}
  im Zusammenhang mit \lstinline{concatenate} und teste diese.
\end{aufgabe}

\begin{aufgabe}
Die folgende Funktion quadriert natürliche Zahlen:
%
\indexvariable{square}
\begin{lstlisting}
(: square (natural -> natural))
(define square
  (lambda (n)
    (cond
     ((zero? n) 0)
     ((positive? n)
      (+ (square (- n 1))
         (- (+ n n) 1))))))
\end{lstlisting}
%
Formuliere dies als Eigenschaft und überprüfe sie mit
\lstinline{check-property}.

\smallskip\noindent
\textbf{Bonus:} Beweise die Eigenschaft mit Induktion.
%
\end{aufgabe}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "i1"
%%% End: