i1prop.tex

% Diese Datei ist Teil des Buchs "Schreibe Dein Programm!"
% Das Buch ist lizensiert 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}

Erinnerst Du Dich noch 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:
%
\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}\index{for-all@\texttt{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}-Ausrdrücke im allgemeinen aufgebaut sind.

\begin{feature}{\lstinline{for-all}}{scheme:for-all}
  \lstinline{For-all}\index{for-all@\texttt{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 von \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} auch 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}\index{check-property@\texttt{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 einmal machen wir aber einen kleinen Exkurs: Was passiert
eigentlich 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 vielen Fällen ist es trotzdem
möglich, Eigenschaften von Funktionen formal zu beweisen.  Das ist
allerdings (noch) meist recht aufwendig.  (Dazu mehr in
Abschnitt~\ref{sec:programme-beweisen} auf
Seite~\pageref{sec:programme-beweisen}.)

\lstinline{Check-property} kann also eine Eigenschaft nicht im
allgemeinen beweisen.  Stattdessen führt es Stichproben durch: Dafür
wählt für die angegebenen Signaturen zufällig Werte aus, und
wiederholt diesen Prozess, um so aus einem Testfall viele individuelle
Tests zu machen~-- typischerweise mehr als 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}

Es geht's 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{==>} allerdings stellt
\lstinline{check-property} sicher, dass tatsächlich 100 Tests
durchgeführt werden, bei denen \lstinline{temp} nicht 0 ist.  Das ist
besser, vor allem bei Tests, bei denen die Bedingung für viele
mögliche Werte gilt, nicht nur für den einen wie hier.
\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 \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{heat->temperature}
\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.  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}
  Versuchen, 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}

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):
%
\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}
%
Für das Sortieren gibt viele Algorithmen, wir machen das mit einem
besonders einfachen, wenn auch ineffizienten Verfahren namens
\textit{Insertionsort}\index{Insertionsort}.  Die Idee ist folgende:
Die Sortierfunktion arbeitet mit einer sortierte 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?

Hier Kurzbeschreibung und Signatur für die Hilfsfunktion zum Einfügen:
%
\begin{lstlisting}
; Bandmitglied in eine sortierte Liste einfügen
(: insert (band-member (list-of band-member) -> (list-of band-member)))
\end{lstlisting}
%
Da dies eine Hilfsfunktion für die eigentliche Sortierfunktion ist,
heben wir uns das Testen ausnahmsweise bis zu dieser auf.
Konstruieren tun wri streng nach Anleitung.  Gerüst und Schablone:
%
\begin{lstlisting}
(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}:
%
\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 haben 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, zum Beispiel um sie schneller zu machen, 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:
%
\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
schonmal 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 bei 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 Wenn es um das Sortieren von Listen geht, dann weißt Du, 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}

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 testet,
ist ziemlich unwahrscheinlich.

Eine weitere grundsätzliche 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. Wenn wir einen \lstinline{check-expect}-Testfall schreiben,
der ein bestimmtes Ergebnis von
\lstinline{balanced-search-tree-insert} erwartet, kann es sein, das
die Funktion ein anders, 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 im Rahmen von
\lstinline{check-property}-Tests zusammen mit
\lstinline{balanced-search-tree-insert} aufrufen und wir hoffen, dass
dies die benötigte Redundanz schafft, was die Korrektheit von
\lstinline{balanced-search-tree-insert} betrifft.  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 Fehler in \lstinline{proper-sized-search-tree?} "<passen"> genau
  zu den Fehlern in \lstinline{balanced-search-tree-insert}.  Um dem
  vorzubeugen, werden wir \lstinline{proper-sized-search-tree?}
  systematisch mit Hilfe der Konstruktionsanleitungen entwickeln.
  Wir werden sehen, dass dies bei
  \lstinline{proper-sized-search-tree?} deutlich einfacher ist als
  \lstinline{balanced-search-tree-insert}.  
  Damit ist es wahrscheinlich, dass
  \lstinline{proper-sized-search-tree?} korrekt gelingt.
\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 ja in dem \lstinline{search-tree}-Record drin.  Den extrahieren
wir und lassen die eigentliche Arbeit von einer 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:
%
\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 ja, um
\lstinline{balanced-search-tree-insert} zu testen.  Wenn die korrekt
ist, dann produziert sie nur solche Suchbäume, bei denen
\lstinline{proper-sized-search-tree?} als Ergebnis \lstinline{#t}
liefert.  Man könnte 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}
%
Um korrekte größenannotatierte Suchbäume zu erzeugen, rufen wir
stattdessen \lstinline{balanced-search-tree-insert} wiederholt auf.
Die Elemente dafür holen wir aus einer Liste und schreiben
entsprechend eine Funktion, die aus einer Liste einen Suchbaum macht.
Kurzbeschreibung und Signatur:
%
\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:
%
\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 \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 ist 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 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 Funktion in allen Tests scheinbar korrekt funktioniert.  Erst,
wenn sie 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?}:
%
\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 schon 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 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 tatsächlich 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.  Falls Du nicht blättern
magst~-- so gehtt es los:
%
\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
\lstinline{check-property}-Testfall 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 Weise zusammenarbeiten.  Schreibe auf, wie diese
  Zusammenarbeit aussieht.
\end{quote}
%
Die Funktion \lstinline{balanced-search-tree-insert} ist ja nur
insofern sinnbvoll, 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~-- strikt nach Konstruktionsanleitung für Listen:
%
\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 schonmal 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}
%
Ganz fertig ist das noch nicht.  Wir müssen noch sicherstellen, dass
\lstinline{number} nicht zufällig doch im Suchbaum ist.  Dazu 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}.

Damit 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.)  Tatsächlich ist die Assoziativität eine Eigenschaft~--
aber wovon?  Zunächst einmal ist sie eine Eigenschaft von $+$ und
$\times$ und cat.  Entsprechend kann man auch sagen "<$+$ ist
assoziativ"> oder "<cat ist assoziativ">.  Die Funktionen $+$,
$\times$ und cat haben allesamt etwas gemeinsam, nämlich die Struktur
ihrer Signaturen.  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 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 integer))
           (b (list integer))
           (c (list integer)))
   (expect (concatenate (concatenate a b) c)
           (concatenate a (concatenate b c)))))
\end{lstlisting}
%
Du fragst Dich vielleicht, warum \lstinline{(list integer)} als
Signatur und nicht \lstinline{(list %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}.)
%
\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 \ref{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} undsoweiter können wir abstrahieren; sie haben
alle die folgende Form:
%
\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 gilt folgende Eigenschaft:
%
\begin{lstlisting}
(for-all ((a $s$))
  (and (expect ($op$ a $n$) a)
       (expect ($op$ $n$ a) a)))
\end{lstlisting}
%
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 integer)))
   (and (expect (concatenate a empty) a)
        (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}\index{empty-image@\texttt{empty-image}}.
%
\begin{aufgabeinline}
  Formuliere \lstinline{check-property}-Testfälle für die
  Neutrales-Element-Eigenschaft von \lstinline{empty-image}.
\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}

\subsection{Binäre Operationen}
\label{sec:eigenschaften-binaere-operationen}

Eine allgemein bekannte Eigenschaft der Addition ist die
\index{Kommutativität}\textit{Kommutativität}:
%
\begin{displaymath}
a + b = b + a
\end{displaymath}
%
Auch wenn intuitiv die Bedeutung klar ist, ist  die Eigenschaft genau
genommen so noch nicht präzise schriftlich festgehalten, da nicht
notiert ist, was $a$ und $b$ sind: Die Idee ist natürlich,
dass $a$ und $b$ beliebige \emph{Zahlen} sind.  Im allgemeinen also:
%
\begin{displaymath}
\forall a \in \mathbb{C}, b \in \mathbb{C}:\ a + b = b + a 
\end{displaymath}
%
(Wer sich mit der Vorstellung komplexer Zahlen nicht wohlfühlt, kann
das $\mathbb{C}$ auch durch $\mathbb{R}$ oder $\mathbb{Q}$ ersetzen.)

FIXME

In den Lehrspachen lässt sich diese Eigenschaft für die eingebaute Funktion
\lstinline{+} aufschreiben~-- das $\forall$ ist auf
Tastaturen nicht vertreten und wird darum ausgeschrieben (siehe
Abbildung~\ref{scheme:for-all}):
%
\begin{lstlisting}
(for-all ((a number)
          (b number))
  (= (+ a b) (+ b a)))
\end{lstlisting}
%

Interessanter wird es erst bei Eigenschaften, die nicht stimmen.  Zum
Beispiel ist die Subtraktion \lstinline{-} nicht kommutativ:
%
\begin{lstlisting}
(check-property
 (for-all ((a number)
           (b number))
   (= (- a b)
      (- b a))))
\end{lstlisting}
%
Hierfür liefert \drscheme{} folgende Meldung:
%
\begin{alltt}
        Eigenschaft falsifizierbar mit a = \framebox{#i1.25} b = \framebox{#i-4.0}
\end{alltt}
%
\textit{Falsifizierbar}\index{falsifizierbar} bedeutet, dass es ein
\textit{Gegenbeispiel\index{Gegenbeispiel}} für die Eigenschaft gibt,
also Werte für die Variablen \lstinline{a} und \lstinline{b}, welche die
Eigenschaft falsch werden lassen.  \drscheme{} hat in diesem Fall ein
Gegenbeispiel gefunden, bei dem \lstinline{a} den Wert \verb|#i1.25| und
\lstinline{b} den Wert \verb|#i-4.0| hat:
%
\begin{lstlisting}
(- #i1.25 #i-4.0)
|\evalsto| #i5.25
(- #i-4.0 #i1.25)
|\evalsto| #i-5.25
\end{lstlisting}
%
Dieses Beispiel widerlegt also tatsächlich die Behauptung der Eigenschaft.

Hinter den Kulissen hat \drscheme{} verschiedene Werte für \lstinline{a} und
\lstinline{b} durchprobiert und in die Eigenschaft eingesetzt, also effektiv
nach einem Gegenbeispiel gesucht.  Für die Kommutativität von
\lstinline{+} gibt es kein Gegenbeispiel~-- \drscheme{} konnte also auch
keins finden.  Dass ausgerechnet das merkwürdige Beispiel $0.0$ und
$-1.5$ herauskam, liegt an der relativ komplexen Suchstrategie von
\drscheme{}.

Auf diese Art und Weise lassen sich eine Reihe von interessanten
Eigenschaften formulieren, so zum Beispiel die Assoziativität\index{Assoziativität} von
\lstinline{+}:\label{sec:plus-not-associative}
%
\begin{lstlisting}
(check-property
 (for-all ((a number)
           (b number)
           (c number))
    (= (+ a (+ b c))
       (+ (+ a b) c))))
\end{lstlisting}
%
Hierbei gibt es allerdings eine böse Überraschung~-- \drscheme{} produziert
ein Gegenbeispiel:

FIXME: inexakte Zahlen

%
\begin{alltt}
Eigenschaft falsifizierbar mit
  a = \framebox{2.6666666666666665} b = \framebox{6.857142857142857} c = \framebox{-6.857142857142857}
\end{alltt}
%
Es ist kein Zufall, dass es sich um Zahlen mit vielen Nachkommastellen
handelt.  Wenn dieses Gegenbeispiel in die Eigenschaft eingesetzt
wird, liefert die REPL folgende Ergebnisse:
%
\begin{lstlisting}
(+ 2.6666666666666665 (+ 6.857142857142857 -6.857142857142857))
|\evalsto| 2.6666666666666665
(+ (+ 2.6666666666666665 6.857142857142857) -6.857142857142857)
|\evalsto| 2.666666666666667
\end{lstlisting}
%
Hier wird sichtbar dass, wie bereits in
Abschnitt~\ref{sec:programming-elements} erwähnt, bei Berechnungen mit
sogenannten \textit{inexakten Zahlen\index{inexakte Zahlen}}, das sind
Zahlen mit einem Dezimalpunkt, die mathematischen Operationen nur mit
einer begrenzten Anzahl von Stellen durchgeführt werden und dann runden~-- da
auch noch binär und nicht dezimal gerundet wird, sieht das Ergebnis
dieser Rundung oft unintuitiv aus.  Dieses Beispiel zeigt nun, dass
Addition plus binäre Rundung nicht assoziativ ist.  Die Assoziativität
gilt nur für das Rechnen mit \textit{exakten Zahlen\index{exakte
    Zahlen}}.  Immerhin sind alle Zahlen mit der Signatur
\lstinline{rational} exakt, die
Eigenschaft lässt sich also reformulieren:
%
\begin{lstlisting}
(check-property
 (for-all ((a rational)
           (b rational)
           (c rational))
    (= (+ a (+ b c))
       (+ (+ a b) c))))
\end{lstlisting}
%
Und tatsächlich, in dieser Form wird die Eigenschaft nicht
beanstandet.

Kommutativität und Assoziativität sind jeweils Eigenschaften einer
einzelnen Operation, in diesem Fall \lstinline{+}.  Manche Eigenschaften
beschreiben auch das Zusammenspiel mehrerer Operationen, wie zum
Beispiel die Distributivität, die für Addition und Multiplikation
gilt:
%
\begin{displaymath}
\forall a \in \mathbb{C}, b \in \mathbb{C}, c \in \mathbb{C}:\
a\times(b+c) = a\times b + b\times c
\end{displaymath}
%
Auch dies lässt sich direkt in Code übersetzen, diesmal gleich mit
\lstinline{rational} statt \lstinline{number}:
%
\begin{lstlisting}
(check-property
 (for-all ((a rational)
           (b rational)
           (c rational))
   (= (* a (+ b c))
      (+ (* a b) (* a c)))))
\end{lstlisting}
%
Auch hier hat \drscheme{} nichts zu meckern.

Neben der Addition ist auch die Multiplikation kommutativ:
%
\begin{lstlisting}
(check-property
 (for-all ((a rational)
           (b rational))
   (= (* a b)
      (* b a))))
\end{lstlisting}
%
Wenn Du diese Eigenschaft neben die Kommutativität für \lstinline{+}
legst, siehst Du, dass diese fast identisch sind und damit natürliche
Kandidaten für Abstraktion: Nur die Operation~-- \lstinline{*} im einen
und \lstinline{+} im anderen Fall~-- ist unterschiedlich.  Wenn wir über
die Operation abstrahieren, bekommen wir so etwas wie eine allgemeine
Definition der Kommutativität, und das sieht so aus:

\begin{lstlisting}
(define commutativity
  (lambda (op)
    (for-all ((a rational)
              (b rational))
      (= (op a b)
         (op b a)))))
\end{lstlisting}
%
Mit Hilfe dieser Definition können wir die Kommutativität von
\lstinline{+} und \lstinline{*} deutlich kompakter formulieren:
%
\begin{lstlisting}
(check-property (commutativity *))
(check-property (commutativity +))
\end{lstlisting}
%
Über dem \lstinline{check-property} können wir nicht abstrahieren~-- es
muss ganz außen stehen, damit \drscheme{} Fehlermeldungen den dazu
passenden Programmstellen zuordnen kann.

Der Vollständigkeit halber braucht \lstinline{commutativity} noch eine
Signatur: \lstinline{+} und \lstinline{*} sind jeweils Funktionen, die zwei
Zahlen akzeptieren und wieder eine Zahl zurückliefern.  Der
Rückgabewert von \lstinline{commutativity} ist eine Eigenschaft, für die
in \drscheme{} die Signatur \lstinline{property} fest eingebaut ist.  Die
fertige Signatur ist also diese hier:
%
\begin{lstlisting}
(: commutativity ((rational rational -> rational) -> property))
\end{lstlisting}

Diese drei Eigenschaften~-- Kommutativität, Assoziativität und
Distributivität~-- tauchen immer wieder auf, da sie nicht nur für
arithmetische Operationen gelten (auch die Multiplikation ist
kommutativ und assoziativ) sondern auch anderswo.  

Zum Beispiel gelten
Kommutativität und Assoziativität auch für das logische \lstinline{and}:
%
\begin{lstlisting}
(check-property
 (for-all ((a boolean)
           (b boolean))
    (boolean=? (and a b)
               (and b a))))

(check-property
 (for-all ((a boolean)
           (b boolean)
           (c boolean))
    (boolean=? (and a (and b c))
               (and (and a b) c))))
\end{lstlisting}
%
Hier muss die eingebaute Funktion \lstinline{boolean=?} verwendet werden,
die boolesche Werte vergleicht, analog zu \lstinline{=}, die nur Zahlen
vergleichen kann.

Schön wäre natürlich, wenn wir auch für die Kommutativität von
\lstinline{and} die obige Funktion \lstinline{commutativity} verwenden
könnten: Das Problem ist aber, dass sich die Kommutativität von
\lstinline{and} an zwei weiteren Stellen von der Kommutativität für
\lstinline{*} und \lstinline{+} unterscheidet, nämlich bei der Signatur
(\lstinline{boolean} statt \lstinline{rational}) und auch bei der
Vergleichsoperation (\lstinline{boolean=?} statt \lstinline{=}).  Um auch
\lstinline{and} in den Einzugsbereich von \lstinline{commutativity} zu
holen, müssen wir also auch noch über diese beiden Werte abstrahieren:
%
\begin{lstlisting}
(define commutativity
  (lambda (op sig =?)
    (for-all ((a sig)
              (b sig))
      (=? (op a b)
          (op b a)))))
\end{lstlisting}
%
Für \lstinline{*} und \lstinline{+} müssen wir \lstinline{commutativity} nun
wie folgt aufrufen:
%
\begin{lstlisting}
(check-property (commutativity * (signature rational) =))
(check-property (commutativity + (signature rational) =))
\end{lstlisting}
%
Denk an das \lstinline{signature}, das immer notwendig ist, wenn
eine Signatur außerhalb einer Signatur-Deklaration mit \lstinline{:} sowie
einem \lstinline{for-all} vorkommt.

Um \lstinline{commutativity} auch auf \lstinline{and} und \lstinline{or}
loszulassen, gibt es allerdings noch ein weiteres Hindernis: Das
Argument zu \lstinline{op} muss eine Funktion sein~-- \lstinline{and} und
\lstinline{or} sind aber Spezialformen.  Wir können sie aber zu
Funktionen machen, indem wir \lstinline{lambda}s darumwickeln:
%
\begin{lstlisting}
(check-property (commutativity (lambda (a b) (and a b))
                               (signature boolean) boolean=?))
(check-property (commutativity (lambda (a b) (or a b))
                               (signature boolean)
                               boolean=?))
\end{lstlisting}
%
Bei der neuen Version von \lstinline{commutativity} fehlt noch die
Signatur.  Wir müssen dazu die ursprüngliche Signatur
%
\begin{lstlisting}
(: commutativity ((rational rational -> rational) -> property))
\end{lstlisting}
%
ziemlich radikal renovieren: Das erste Argument ist zwar immer noch
eine zweistellige Funktion, aber nicht mehr notwendigerweise auf
rationalen Zahlen.  Wir skizzieren erstmal, was wir wissen:
%
\begin{lstlisting}
(: commutativity ((? ? -> ?) signature (? ? -> boolean) -> property))
\end{lstlisting}
%
Die eingebaute Signatur \lstinline{signature} ist für Signaturen
zuständig~-- das zweite Argument ist ja eine Signatur.  Von der
Vergleichsfunktion an dritter Stelle ist klar, dass sie ein
\lstinline{boolean} liefert.  Für die restlichen Fragezeichen ist die
genaue Signatur abhängig vom konkreten Operator und dieser (ebenfalls
variablen) Signatur, wir müssen also Signaturvariablen verwenden.

Was ist noch bekannt?  Die beiden Argumente der Funktion \lstinline{op}
müssen auf dieselbe Signatur passen, da sie ja vertauschbar sind:
%
\begin{lstlisting}
(: commutativity ((%a %a -> ?) signature (? ? -> boolean) -> property))
\end{lstlisting}
%
Außerdem wird der Rückgabewert von \lstinline{op} in die
Vergleichsfunktion gefüttert, für die restliche drei Fragezeichen
müssen wir also dieselbe Signatur einsetzen.  Ist erforderlich, dass
der Rückgabewert von \lstinline{op} auf die gleiche Signatur passt wie die
Argumente?  Der Rückgabewert wird nicht wieder in \lstinline{op}
hineingefüttert, die Antwort ist also nein.  Wir können also eine
von \lstinline{%a} verschiedene Signaturvariable benutzen:
%
\begin{lstlisting}
(: commutativity ((%a %a -> %b) signature (%b %b -> boolean) -> property))
\end{lstlisting}
%
Genauso wie bei der Kommutativität können wir auch bei der
Assoziativität abstrahieren.  Hier die Abstraktion, die dabei
herauskommt:
%
\begin{lstlisting}
(define associativity
  (lambda (op sig =?)
    (for-all ((a sig)
              (b sig)
              (c sig))
      (=? (op a (op b c))
          (op (op a b) c)))))
\end{lstlisting}
%
Benutzen können wir sie ähnlich wie bei der Kommutativität:
%
\begin{lstlisting}
(check-property (associativity + (signature rational) =))
(check-property (associativity * (signature rational) =))
(check-property (associativity (lambda (a b) (and a b))
                               (signature boolean)
                               boolean=?))
(check-property (associativity (lambda (a b) (or a b))
                               (signature boolean)
                               boolean=?))
\end{lstlisting}
%
Auch hier die Formulierung der Signatur nicht so einfach.  Die erste
Skizze könnte so aussehen:
%
\begin{lstlisting}
(: associativity ((? ? -> ?) signature (? ? -> boolean) -> property))
\end{lstlisting}
%
Wie bei \lstinline{commutativity} wird der Rückgabewert von \lstinline{op}
als Argument für die Vergleichsfunktion verwendet: Die letzten drei
Fragezeichen müssen also wieder gleich sein.  Anders als bei der
Kommutativität wird der Rückgabewert von \lstinline{op} auch wieder als
Argument in \lstinline{op} hereingefüttert.  Damit müssen auch die ersten
beiden Fragezeichen den anderen entsprechen.  Die beste Signatur ist
also wie folgt:
%
\begin{lstlisting}
(: associativity ((%a %a -> %a) signature (%a %a -> boolean) -> property))
\end{lstlisting}
%
\lstinline{And} und
\lstinline{or} erfüllen auch zwei Distributivgesetze.  Damit beschäftigt
sich Aufgabe~\ref{aufgabe:boolean-distrib}.

Auch das \textrm{DeMorgan'sche Gesetz\index{DeMorgan'sches Gesetz}}
(siehe Abschnitt~\ref{sec:aussagenlogik}) können wir als Code
formulieren:
%
\begin{lstlisting}
(check-property
 (for-all ((a boolean)
           (b boolean))
   (boolean=? (not (and a b))
              (or (not a) (not b)))))
\end{lstlisting}
%
Bei vielen Operationen ist außerdem interessant, ob sie ein
\textit{neutrales Element\index{neutrales Element}} besitzen, also ein
Argument, das dafür sorgt, dass die Operation ein anderes Argument
unverändert zurückgibt.  Die Addition hat z.B.\ die $0$ als neutrales
Element:
%
\begin{lstlisting}
(check-property
  (for-all ((a rational))
    (= (+ a 0) a)))
\end{lstlisting}
%
Streng genommen ist damit nur gesichert, dass $0$ \textit{rechtsneutrales
  Element} ist, also von rechts addiert das andere Argument
unverändert herauskommt.  Aus der Kommutativität folgt aber, dass jedes
rechtsneutrale Element auch ein linksneutrales Element ist.

Bei manchen Operationen gibt es neben dem neutralen Element zu jedem
Element auch ein \textit{inverses Element\index{inverses Element}}:
Wenn eine binäre Operation auf ein Element und sein Inverses
angewendet wird, so muss das neutrale Element herauskommen.  Bei der
Addition entsteht das Inverse zu einer Zahl durch Umdrehen des
Vorzeichens:
%
\begin{lstlisting}
(check-property
 (for-all ((a rational))
   (= (+ a (- a)) 0)))

(check-property
 (for-all ((a rational))
   (= (+ (- a) a) 0)))
\end{lstlisting}
%
Hier noch einmal eine Zusammenfassung der in diesem Abschnitt
behandelten Eigenschaften, mit Kurzfassungen der mathematischen
Formulierungen:

\begin{mantra}[Eigenschaften von binären Operationen]
%
Folgende Eigenschaften sind prinzipiell auf alle \textit{binären}
Operationen denkbar, die zwei Elemente einer Menge $M$ akzeptieren
und wiederum ein Element von $M$ zurückgeben.
\begin{itemize}
\item Kommutativität $a \star b = b \star a$
\item Assoziativität $(a \star b) \star c = a \star (b \star c)$
\item Distributivität $a \otimes (b \star c) = (a \otimes b) \star (a
  \otimes c)$; $(b \star c) \otimes a = (b \otimes a) \star (c
  \otimes a)$
\item neutrales Element ($a\star \nu = a$; $\nu\star a = a$)
\item inverses Element $a\star a^{-1} = \nu$; $a^{-1}\star a = \nu$
\end{itemize}
\end{mantra}

\subsection{Eigenschaften von binären Prädikaten}

FIXME: Begriff Prädikat

Die Funktion \lstinline{=} passt nicht in das Schema der Eigenschaften
des folgenden Abschnitts.  Sie hat folgende Signatur:
%
\begin{lstlisting}
(: = (number number -> boolean))
\end{lstlisting}
%
Damit akzeptiert sie zwar zwei Argumente aus derselben Menge, liefert
aber einen booleschen Wert zurück.  Stattdessen handelt es sich um ein
\textit{binäres Prädikat\index{binäres
    Prädikat}\index{Prädikat!binär}} beziehungsweise eine \textit{binäre
  Relation\index{binäre Relation}\index{Relation!binär}}.  Für binäre
Relationen kommt ein anderer Satz von Eigenschaften in Frage.  (Die
mathematische Seite ist in Anhang~\ref{sec:relationen} beschrieben.)
Insbesondere ist \lstinline{=} eine
\textit{Äquivalenzrelation\index{Äquivalenzrelation}} und damit
\textit{reflexiv\index{reflexiv}},
\textit{symmetrisch\index{symmetrisch}} und
\textit{transitiv\index{transitiv}}.

Die Reflexivität besagt, dass jedes Element der Grundmenge (in diesem
Fall die Menge der Zahlen) zu sich selbst in Beziehung steht:
%
\begin{lstlisting}
(check-property
 (for-all ((a number))
   (= a a)))
\end{lstlisting}
%
Die Symmetrie bedeutet für \lstinline{=}, dass aus
\lstinline{(= a b) |\evalsto| #t} das "<Spiegelbild">
\lstinline{(= b a) |\evalsto| #t}
folgt.  Mathematisch geschrieben sähe das so aus:
%
\begin{displaymath}
  \forall a \in \mathbb{C}, b\in\mathbb{C}:\ a = b \Rightarrow b = a
\end{displaymath}
%
\begin{feature}{\lstinline{==>}}{scheme:implies}

Eine \textit{Implikation}\index{Implikation} in einer Eigenschaft wird
folgendermaßen geschrieben:
\begin{lstlisting}
(==> $e$ $e\sb{p}$)
\end{lstlisting}
%
Dabei muss $e$ ein Ausdruck mit booleschem Wert sein (die
\textit{Voraussetzung}) und $e\sb{p}$ eine Eigenschaft oder ein
boolescher Ausdruck.  Die Implikation liefert ihrerseits wieder eine
Eigenschaft, die gilt, wenn $e\sb{p}$ immer dann gilt, wenn die
Voraussetzung erfüllt ist, also \lstinline{#t} liefert.
\end{feature}

Der Implikationspfeil $\Rightarrow$ wird in den Lehrsprachen
\lstinline{==>}\index{==>@\texttt{==>}} geschrieben.  (Siehe
Abbildung~\ref{scheme:implies}.)  Der Test der
Symmetrie sieht also folgendermaßen aus:
%
\begin{lstlisting}
(check-property
 (for-all ((a number)
           (b number))
   (==> (= a b)
        (= b a))))
\end{lstlisting}
%
Ähnlich läuft es mit der Transitivität: Wenn zwei Zahlen $a$ und $b$
gleich sind sowie $b$ und eine dritte Zahl $c$, dann müssen auch $a$
und $c$ gleich sein:
%
\begin{lstlisting}
(check-property
 (for-all ((a number)
           (b number)
           (c number))
   (==> (and (= a b) (= b c))
        (= a c))))
\end{lstlisting}
%
Neben den drei Eigenschaften von Äquivalenzrelationen tritt auch
gelegentlich die Eigenschaft
\textit{Antisymmetrie}\index{antisymmetrisch} auf (die mathematische
Definition steht in Anhang~\ref{sec:relationen}).

\begin{mantra}[Eigenschaften von binären Prädikaten]
%
Folgende Eigenschaften sind für binäre Prädikate denkbar:
\begin{itemize}
\item Reflexivität $a \leftrightsquigarrow a$
\item Symmetrie $a \leftrightsquigarrow b \Rightarrow b \leftrightsquigarrow a$
\item Transitivität $a \leftrightsquigarrow b \wedge b
  \leftrightsquigarrow c
  \Rightarrow a \leftrightsquigarrow c$
\item Antisymmetrie $a \leftrightsquigarrow b \wedge  b
  \leftrightsquigarrow a \Rightarrow a = b$
\end{itemize}
\end{mantra}

\section{Eigenschaften von Funktionen auf Listen}

Es wird Zeit, Eigenschaften von selbstgeschriebenen Funktionen zu
überprüfen.  In diesem Abschnitt geht es um einige der Funktionen, die
auf Listen operieren: \lstinline{concatenate}, \lstinline{invert},
und \lstinline{list-sum}.

\subsection{Eigenschaften von \lstinline{concatenate}}

Die Funktion
\lstinline{concatenate}\index{concatenate@texttt{concatenate}} aus
Abschnitt~\ref{sec:concatenate} hängt zwei Listen aneinander.  Auch
\lstinline{concatenate} ist assoziativ: Wenn drei Listen mit Hilfe von
\lstinline{concatenate} aneinandergehängt werden, spielt es keine Rolle,
ob zuerst die ersten beiden oder zuerst die letzten beiden Listen
aneinandergehängt werden.  Nach dem Muster der Assoziativität von
\lstinline{+} und \lstinline{and} sieht der Test dieser Eigenschaft
folgendermaßen aus:
%
\begin{lstlisting}
(check-property
 (associativity concatenate (signature (list-of number)) |\ldots|))
\end{lstlisting}
%
Beim Test ist die Signatur von \lstinline{lis-1}, \lstinline{lis-2} und
\lstinline{lis-3} jeweils \lstinline{(list-of number)}.  Die Signatur von \lstinline{concatenate}
%
\begin{lstlisting}
(: concatenate ((list-of %a) (list-of %a) -> (list-of %a)))
\end{lstlisting}
%
suggeriert allerdings, dass die Signatur von \lstinline{lis-1},
\lstinline{lis-2} und \lstinline{lis-3} jeweils \lstinline{(list-of \%a)} lauten
sollte, also allgemeiner als \lstinline{(list-of number)}.  Signaturen mit
Signaturvariablen funktionieren allerdings nicht im Zusammenhang mit
Eigenschaften, wie folgendes Beispiel zeigt:
%
\begin{lstlisting}
(check-property
  (for-all ((x %a))
    ...))
\end{lstlisting}
%
Dieser Code liefert die Fehlermeldung "<Signatur hat keinen
Generator">: Das liegt daran, dass die Signaturvariable \lstinline{%a}
zuwenig Information über die zugrundeliegenden Werte liefert, als dass
\drscheme{} sinnvoll Werte für die Tests generieren könnte.  Aus diesem
Grund müssen in \lstinline{for-all} immer "<konkrete"> Signaturen ohne
Signaturvariablen angegeben werden.  (Aus ähnlichen Gründen
funktionieren auch einige andere Arten von Signaturen nicht bei
\lstinline{for-all}, inbesondere Record-Signaturen.  Funktionsignaturen sind
allerdings zulässig und werden in Abschnitt~\ref{sec:ho-props} behandelt.)

Für \lstinline{concatenate} wäre es zwar gründlicher, die Tests auch noch
für andere Sorten von Listenelementen als \lstinline{number}
durchzuführen~-- da aber \lstinline{concatenate} mit den Listenelementen
nichts anfängt, außer sie in weitere Liste zu stecken, reicht die
Formulierung der Eigenschaft mit \lstinline{(list-of number)} aus.

Es bleibt noch ein weiteres Problem bei der Formulierung der
Assoziativität für \lstinline{concatenate}: Es steht noch keine Funktion
für den Vergleich der beiden Listen zur Verfügung, die muss erst noch
geschrieben werden.  Kurzbeschreibung und
Signatur:\index{number-list=?@texttt{number-list=?}}
%
FIXME: über = abstrahieren
%
\begin{lstlisting}
; Zwei Listen aus Zahlen vergleichen
(: number-list=? ((list-of number) (list-of number) -> boolean))
\end{lstlisting}
%
Die Testfälle sollten insbesondere Listen unterschiedlicher Länge
berücksichtigen:
%
\begin{lstlisting}
(check-expect (number-list=? empty empty) #t)
(check-expect (number-list=? (list 1.0 2.0 3.0) (list 1.0 2.0 3.0)) #t)
(check-expect (number-list=? (list 1.0 2.0 3.0) (list 1.0 2.0)) #f)
(check-expect (number-list=? (list 1.0 2.0) (list 1.0 2.0 3.0)) #f)
(check-expect (number-list=? (list 1.0 2.0 3.0) (list 1.0 2.1 3.0)) #f)
\end{lstlisting}
%
Die Schablone für Listen als Eingabe, ausgewählt nach dem ersten Listenparameter
\lstinline{lis-1}, sieht so aus:
% 
\begin{lstlisting}
(define number-list=?
  (lambda (lis-1 lis-2)
    (cond
      ((empty? lis-1)
       ...)
      ((cons? lis-1)
       ... (first lis-1) ...
       ... (number-list=? (rest lis-1) ...) ...))))
\end{lstlisting}
%
Die Schablone für den zweiten Listenparameter \lstinline{lis-2} wird in
beide Zweige des \lstinline{cond} eingesetzt:
%
\begin{lstlisting}
(define number-list=?
  (lambda (lis-1 lis-2)
    (cond
      ((empty? lis-1)
       (cond
         ((empty? lis-2) ...)
         ((cons? lis-2)
          ... (first lis-2) ...
          ... (number-list=? ... (rest lis-2)))))
      ((cons? lis-1)
       ... (first lis-1) ...
       ... (number-list=? (rest lis-1) ...) ...
       (cond
         ((empty? lis-2) ...)
         ((cons? lis-2)
          ... (first lis-2) ...
          ... (number-list=? ... (rest lis-2))))))))
\end{lstlisting}
%
Es gibt also insgesamt vier Fälle bei den Verzweigungen:
\begin{itemize}
\item Im ersten
Fall sind beide Listen leer, das Ergebnis ist also \lstinline{#t}.
\item Im zweiten Fall ist die erste Liste leer und die zweite
  nichtleer.  Das Ergebnis ist also \lstinline{#f} und die
  Schablonenelemente sind überflüssig.
\item Im dritten Fall ist die erste Liste nichtleer und die zweite
  leer.  Das Ergebnis ist also wiederum \lstinline{#f}.
\item Im vierten Fall sind beide Listen nichtleer und in der Schablone
  stehen die jeweils ersten Elemente von \lstinline{lis-1} und
  \lstinline{lis-2}.  Die beiden Listen sind nur gleich, wenn die beiden
  ersten Elemente gleich sind.  Außerdem müssen natürlich die beiden
  Reste der Listen ebenfalls gleich sind~-- die beiden rekursiven
  Aufrufe aus den Schablonen können also kombiniert werden:
\end{itemize}
%
\begin{lstlisting}
(define number-list=?
  (lambda (lis-1 lis-2)
    (cond
      ((empty? lis-1)
       (cond
         ((empty? lis-2) #t)
         ((cons? lis-2) #f)))
      ((cons? lis-1)
       (cond
         ((empty? lis-2) #f)
         ((cons? lis-2)
          (and (= (first lis-1) (first lis-2))
               (number-list=? (rest lis-1) (rest lis-2)))))))))
\end{lstlisting}
%
Damit kann jetzt die Assoziativität von \lstinline{concatenate} getestet werden:
%
\begin{lstlisting}
(check-property
 (associativity concatenate (signature (list-of number)) number-list=?))
\end{lstlisting}
%
\lstinline{Concatenate} hat außerdem ein neutrales Element, und zwar
sowohl im linken als auch im rechten Argument:
%
\begin{lstlisting}
(check-property
 (for-all ((lis (list-of number)))
   (number-list=? lis (concatenate empty lis))))

(check-property
 (for-all ((lis (list-of number)))
   (number-list=? lis (concatenate lis empty))))
\end{lstlisting}
%
\lstinline{Concatenate} ist allerdings demonstrierbar nicht kommutativ.
Der entsprechende Test sieht so aus:
%
\begin{lstlisting}
(check-property
 (commutativity concatenate (signature (list-of number)) number-list=?))
\end{lstlisting}
%
\drscheme{} liefert hierfür ein Gegenbeispiel:
%
\begin{alltt}
Eigenschaft falsifizierbar mit
         lis-1 = \framebox{#<list -3.75>} lis-2 = \framebox{#<list 1.5 1.5>}
\end{alltt}

\subsection{Eigenschaften von \lstinline{number-list=?}}

Wie der Zufall so will, hat auch die Hilfsfunktion
\lstinline{number-list=?} interessante Eigenschaften: Wie \lstinline{=} muss
auch \lstinline{number-list=?} eine Äquivalenzrelation sein~--
schließlich testet sie wie \lstinline{=} auf Gleichheit.  Die
dazugehörigen Eigenschaften~-- Reflexivität, Symmetrie und
Transitivität~-- können ebenso wie bei \lstinline{=} formuliert werden:

Reflexivität:
%
\begin{lstlisting}
(check-property
 (for-all ((lis (list-of number)))
   (number-list=? lis lis)))
\end{lstlisting}
Symmetrie:
\begin{lstlisting}
(check-property
  (for-all ((lis-1 (list-of number))
            (lis-2 (list-of number)))
    (==> (number-list=? lis-1 lis-2)
         (number-list=? lis-2 lis-1))))
\end{lstlisting}
 Transitivität
\begin{lstlisting}
(check-property
 (for-all ((lis-1 (list-of number))
           (lis-2 (list-of number))
           (lis-3 (list-of number)))
   (==> (and (number-list=? lis-1 lis-2)
             (number-list=? lis-2 lis-3))
        (number-list=? lis-1 lis-3))))
\end{lstlisting}
%

\subsection{Eigenschaften von \lstinline{invert}}

Die Funktion \lstinline{invert} aus Abschnitt~\ref{sec:invert} dreht die
Reihenfolge der Elemente einer Liste um.  Eine naheliegende
Eigenschaft von \lstinline{invert} ist, dass zweimaliges Umdrehen wieder
die Ursprungsliste liefern sollte:
%
\begin{lstlisting}
(check-property
 (for-all ((lis (list-of number)))
   (number-list=? lis (invert (invert lis)))))
\end{lstlisting}
%
Auch bei \lstinline{invert} enthält die Signatur eine Signaturvariable:
%
\begin{lstlisting}
(: invert ((list-of %a) -> (list-of %a)))
\end{lstlisting}
%
Genau wie bei \lstinline{concatenate} macht \lstinline{invert} mit den
Listenelementen nichts spezielles, es können also auch zum Beispiel Zeichenketten
benutzt werden.  Diese Änderung allein funktioniert allerdings nicht:
%
\begin{lstlisting}
(check-property
 (for-all ((lis (list-of string)))
   (\textbf{number-list=?} lis (invert (invert lis)))))
\end{lstlisting}
%
Die Funktion \lstinline{number-list=?} funktioniert nur auf Listen von
Zahlen.  Es wäre möglich, \lstinline{number-list=?} über der
Vergleichsfunktion auf den Elementen zu abstrahieren, aber es wäre
trotzdem umständliche Arbeit nur für den Zweck des Testens.  Deshalb 
gibt es eine Vereinfachung analog zu \lstinline{check-expect}.  Die eingebaute Form \lstinline{expect}
akzeptiert zwei beliebige Werte und ist dann erfüllt, wenn diese Werte
gleich sind.  (Siehe Abbildung~\ref{scheme:expect}.)  Die Eigenschaft
von \lstinline{invert} sieht damit so aus:

\begin{feature}{\lstinline{expect}}{scheme:expect}
  \lstinline{Expect}\index{expect@\texttt{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.

\end{feature}

\begin{lstlisting}
(check-property
 (for-all ((lis (list-of string)))
   (expect lis (invert (invert lis)))))
\end{lstlisting}
%
Viele Funktionen auf Listen haben Eigenschaften, welche die Funktion
jeweils im Zusammenspiel mit einer oder mehreren anderen Funktionen
zeigen.  Bei Funktionen mit Listen ist es häufig interessant, das
Zusammenspiel mit \lstinline{concatenate} zu betrachten.  Damit
\lstinline{concatenate} etwas sinnvolles tun kann, sind zwei Listen
notwendig:
%
\begin{lstlisting}
(check-property
  (for-all ((lis-1 (list-of number))
            (lis-2 (list-of number)))
    ...))
\end{lstlisting}
%
Auf diese zwei Listen kann \lstinline{concatenate} aber auch jeweils
\lstinline{invert} angewendet werden:
%
%
\begin{lstlisting}
(check-property
  (for-all ((lis-1 (list-of number))
            (lis-2 (list-of number)))
    ... (invert lis-1) ...
    ... (invert lis-2) ...
    ... (invert (concatenate lis-1 lis-2)) ...))
\end{lstlisting}
%
Wie lässt sich die Liste \lstinline{(invert (concatenate lis-1 lis-2))}
noch beschreiben?
Angenommen, \lstinline{lis-1} ist die Liste \lstinline{#<list 1 2 3>} und
\lstinline{lis-2} die Liste \lstinline{#<list 4 5 6>}.  Dann gilt:
%
\begin{lstlisting}
(invert (concatenate lis-1 lis-2))
$=$
(invert (concatenate #<list 1 2 3> #<list 4 5 6>))
$\Longrightarrow$ |\ldots| $\Longrightarrow$ (invert #<list $\underbrace{\texttt{1 2 3}}\sb{\texttt{lis-1}}$ $\underbrace{\texttt{4 5 6}}\sb{\texttt{lis-2}}$>))

$\Longrightarrow$ |\ldots| $\Longrightarrow$ #<list $\underbrace{\texttt{6 5 4}}\sb{\texttt{(invert lis-2)}}$ $\underbrace{\texttt{3 2 1}}\sb{\texttt{(invert lis-1)}}$>
\end{lstlisting}
%
Dies lässt vermuten, dass die gesuchte Eigenschaft folgendermaßen aussieht:
%
\begin{lstlisting}
(check-property
 (for-all ((lis-1 (list-of number))
           (lis-2 (list-of number)))
   (expect (invert (concatenate lis-1 lis-2))
           (concatenate (invert lis-2) (invert lis-1)))))
\end{lstlisting}
%
\begin{mantra}[Eigenschaften von Funktionen auf Listen]
  Funktionen, die Listen akzeptieren, haben häufig interessante
  Eigenschaften im Zusammenspiel mit \lstinline{concatenate}.
\end{mantra}

\subsection{Eigenschaften von \lstinline{list-sum}}

\lstinline{List-sum}\index{list-sum@\texttt{list-sum}} aus
Abschnitt~\ref{sec:list-sum} ist, wie \lstinline{invert}, eine Funktion,
die eine Liste akzeptiert.  Genau wie bei \lstinline{invert} ist es eine
gute Idee, die Interaktion zwischen \lstinline{list-sum} und
\lstinline{concatenate} zu untersuchen.  Es müssen also wieder zwei
Listen her~-- die zu \lstinline{invert} analoge Vorgehensweise liefert
folgende Schablone:
%
\begin{lstlisting}
(check-property
 (for-all ((lis-1 (list-of number))
           (lis-2 (list-of number)))
    ... (list-sum lis-1) ...
    ... (list-sum lis-2) ...
    ... (list-sum (concatenate lis-1 lis-2)) ...
\end{lstlisting}
%
Da \lstinline{list-sum} die Elemente der Liste addiert und die Addition
assoziativ ist, müsste folgendes gelten:
%
\begin{lstlisting}
(check-property
 (for-all ((lis-1 (list-of number))
           (lis-2 (list-of number)))
    (expect (+ (list-sum lis-1) (list-sum lis-2))
            (list-sum (concatenate lis-1 lis-2)))))
\end{lstlisting}
%
Hier allerdings schlägt das Rundungsproblem aus
Abschnitt~\ref{sec:plus-not-associative} wieder zu: Die Addition auf
\lstinline{number} ist eben \emph{nicht} assoziativ, aber immerhin auf
\lstinline{rational}.  Der fertige Test muss also so aussehen:
%
\begin{lstlisting}
(check-property
 (for-all ((lis-1 (list-of rational))
           (lis-2 (list-of rational)))
    (expect (+ (list-sum lis-1) (list-sum lis-2))
            (list-sum (concatenate lis-1 lis-2)))))
\end{lstlisting}
%
Eine Alternative ist die Verwendung der Form
\lstinline{expect-within}\index{expect-within@\texttt{expect-within}},
die eine Eigenschaft analog zu \lstinline{check-within} erzeugt.  (Siehe
Abbildung~\ref{scheme:expect-within}.)

\begin{feature}{\lstinline{expect-within}}{scheme:expect-within}
  \lstinline{Expect-within}\index{expect-within@\texttt{expect-within}} liefert eine
  Eigenschaft analog zur Funktionsweise von
  \lstinline{check-within}.  Ein \lstinline{expect-within}-Ausdruck hat folgende
  Form:
  %
\begin{lstlisting}
(expect-within $e\sb{1}$  $e\sb{2}$ $e\sb{\delta}$)
\end{lstlisting}
%
$e_1$, $e_2$ und $e\sb{\delta}$ sind Ausdrücke, wobei $e\sb{\delta}$
eine reelle Zahl liefern muss.  Die resultierende Eigenschaft ist
erfüllt, wenn $e_1$ und $e_2$ den gleichen Wert liefern~-- der
Vergleich wird dabei wie bei \lstinline{check-within} angestellt, das heißt
alle inexakten Zahlen in den Ergebnissen von $e_1$ und $e_2$ müssen
nicht gleich sein, dürfen sich aber höchstens um $e\sb{\delta}$
voneinander unterscheiden.
\end{feature}

Mit \lstinline{expect-within} sieht der Testfall folgendermaßen aus:
%
\begin{lstlisting}
(check-property
 (for-all ((lis-1 (list-of number))
           (lis-2 (list-of number)))
    (expect-within (+ (list-sum lis-1) (list-sum lis-2))
                   (list-sum (concatenate lis-1 lis-2))
                   0.1)))
\end{lstlisting}
%
Auch dieser Testfall läuft durch.

Auch der Test für die Assoziativität von \lstinline{+} aus
Abschnitt~\ref{sec:plus-not-associative} kann mit
\lstinline{expect-within} formuliert werden:
%
\begin{lstlisting}
(check-property
 (for-all ((a number)
           (b number)
           (c number))
    (expect-within (+ a (+ b c))
                   (+ (+ a b) c)
                   0.1)))
\end{lstlisting}
%
So wie sich die Assoziativität von \lstinline{+} in einer Eigenschaft von
\lstinline{list-sum} niederschlägt, tut dies auch die Kommutativität: Sie
besagt, dass die Reihenfolge der Elemente der Liste keine Rolle spielt.
Eine einfache Möglichkeit, dies zu testen, ist wiederum mit zwei
Listen zu arbeiten und diese einmal in der einen und dann in der
anderen Richtung aneinanderzuhängen:\label{sec:list-sum-commutative}
%
\begin{lstlisting}
(check-property
 (for-all ((lis-1 (list-of rational))
           (lis-2 (list-of rational)))
   (expect (list-sum (concatenate lis-1 lis-2))
           (list-sum (concatenate lis-2 lis-1)))))
\end{lstlisting}

\section{Eigenschaften von Funktionen höherer Ordnung}
\label{sec:ho-props}

In Abschnitt~\ref{sec:currying} wurde bereits eine Eigenschaft von
\lstinline{curry}\index{curry@\texttt{curry}} und
\lstinline{uncurry}\index{uncurry@\texttt{uncurry}} aufgeführt:
%
\begin{center}
  \texttt{(uncurry (curry $p$)) $\equiv$ $p$}
\end{center}
%
Mit anderen Worten: \lstinline{curry} und \lstinline{uncurry} sind jeweils
Inverse voneinander.  Auch diese Eigenschaft lässt sich direkt mit
\lstinline{check-property} und \lstinline{for-all} formulieren.  Zu beachten
ist wieder, obwohl \lstinline{curry} und \lstinline{uncurry} polymorphe
Signaturen mit Signaturvariablen haben, dass für den Test mit
\lstinline{check-property} eine "<konkrete"> Signatur ohne
Signaturvariablen für das Funktion-Argument benutzt werden muss, also
zum Beispiel \lstinline{string}:
%
\begin{lstlisting}
(check-property
 (for-all ((proc (string string -> string)))
   (expect (curry (uncurry proc))
           proc)))
\end{lstlisting}
%
Leider schlägt dieser Test fehl, und zwar mit einer mysteriösen
Meldung:
%
\begin{alltt}
Eigenschaft falsifizierbar mit \framebox{#<procedure:?>}
\end{alltt}
%
Offenbar ist \drscheme{} also der Ansicht, es hat eine Funktion gefunden,
welche die Eigenschaft nicht erfüllt, kann aber nicht genau sagen,
welche Funktion: Das liegt daran, dass es prinzipiell unmöglich ist,
zwei Funktionen auf Gleichheit zu überprüfen~-- Gleichheit zweier
Funktionen heißt ja, dass die eine Funktion angewendet auf einen Satz
Argumente \emph{immer} das gleiche Ergebnis wie die andere Funktion
liefert.  Im obigen Beispiel akzeptiert \lstinline{proc} zwei
Zeichenketten, von denen es unendlich viele gibt; die Gleichheit zu
überprüfen, würde also unendlich lange dauern.  \lstinline{Expect}
versucht es darum gar nicht erst, sondern sieht es als notwendige
(nicht als hinreichende) Bedingung für die Gleichheit zweier
Funktionen an, dass sie Wert desselben \lstinline{lambda}-Ausdrucks sind.
\lstinline{Expect} testet also bei Funktionen auf sogenannte
\textit{intensionale Gleichheit}\index{intensionale
  Gleichheit}\index{Gleichheit!intensional}, was soviel heißt, dass
\lstinline{expect} vergleicht, \emph{auf welche Weise} die beiden
Funktionen entstanden sind, nicht aber, ob sich die beiden Funktionen
\emph{gleich verhalten}.  Die letztere Eigenschaft heißt \textit{extensionale
  Gleichheit}\index{Gleichheit!extensional}\index{extensionale
  Gleichheit}~-- und ist, wie gesagt, nicht effektiv testbar.

Der \lstinline{lambda}-Ausdruck der Funktion, die von
\lstinline{(curry (uncurry proc))} geliefert wird, ist aber der Rumpf von
\lstinline{curry}, während der \lstinline{lambda}-Ausdruck von \lstinline{proc}
i.d.R.\ woanders steht; damit sind die beiden Funktionen intensional
ungleich, und der obige Test muss fehlschlagen, auch wenn die beiden
Operanden von \lstinline{expect} äquivalent sind.

Damit ein \lstinline{check-property}-Test die Äquivalenz testen kann, muss
er selbst \lstinline{(curry (uncurry proc))} anwenden:
%
\begin{lstlisting}
(check-property
 (for-all ((a string)
           (b string)
           (proc (string string -> string)))
    (expect ((uncurry (curry proc)) a b)
            (proc a b))))
\end{lstlisting}
%
Dieser Test funktioniert.

\section{Programme beweisen}
\label{sec:programme-beweisen}

\lstinline{Check-property} ist nützlich, um zu überprüfen, ob eine
Eigenschaft gilt oder nicht.  Da \lstinline{check-property} allerdings
nur eine endliche Menge zufälliger Tests durchführt, reicht es nicht
aus, um sicherzugehen, dass eine bestimmte Eigenschaft für alle Werte
der \lstinline{for-all}-Variablen gilt: Dazu ist ein mathematischer
Beweis notwendig.

An verschiedenen Stellen im Buch wurden Beweise für mathematische
Funktionen durchgeführt~-- zuletzt in Kapitel~\ref{cha:indu} für
eine rekursive Funktion.  Beweise über mathematische Funktionen
erlauben, bei jedem Schrittan beliebigen Stellen Gleichungen
einzusetzen.  Beweise über Funktionen in Programmen sind schwieriger,
da sie das Substitutionsmodell berücksichtigen müssen: Bei jedem
Reduktionsschritt kommt immer nur eine bestimmte Substitution in
Frage.

\subsection{Arithmetische Gesetze beweisen}
\label{sec:scheme-arithmetik-beweis}

Als erstes Beispiel für den Beweis an einem Programm dient der Beweis
der Kommutativität von \lstinline{+}.  Der Beweis ist nicht besonders
tiefgreifend, demonstriert aber die wichtigsten Techniken, die beim
Beweisen von Programmen zum Einsatz kommen.  Zu beweisen ist:
%
\begin{lstlisting}
(= (+ a b) (+ b a))
$\Longrightarrow\ldots\Longrightarrow$ #t
\end{lstlisting}
%
\ldots{} und zwar für beliebige Bindungen von \lstinline{a} und
\lstinline{b} an Zahlen.  Seien die Zahlen, die an \lstinline{a} beziehungsweise
\lstinline{b} gebunden sind, $x$ und $y$ mit $x,y\in\mathbb{C}$.  (Die
"<mathematischen"> Namen könnten auch $a$ und $b$ sein, aber das birgt
ein Verwirrungsrisiko mit \lstinline{a} und \lstinline{b}.)  Wenn nun also
der obige Term für bestimmte Werte von $x$ und $y$ im
Substitutionsmodell reduziert wird, wird zuerst $x$ für \lstinline{a} und
$y$ für \lstinline{b} eingesetzt.  Für $x=5$ und $y=17$ also:
%
\begin{lstlisting}
(= (+ 5 17) (+ 17 5))
\end{lstlisting}
%
FIXME: \valof{\_} schwierig

Der Beweis soll aber für beliebige Werte für $x$ und $y$
funktionieren: $x$ und $y$ müssen also im Beweis auftauchen.
Um den Unterschied zwischen Variablen des Programms \lstinline{a} und
\lstinline{b} und den Zahlen zu machen, die für $x$ und $y$ eingesetzt
werden, werden diese noch mit \valof{\_} umgeben: \valof{x} in
einem Reduktionsschritt des Substitutionsmodell ist also ein
Platzhalter für "<die Zahl, für die $x$ steht">~-- entsprechend für $y$.
Es gilt also:

\begin{lstlisting}
(= (+ a b) (+ b a))
$=$ (= |\redex{(+ \valof{x} \valof{y})}| (+ |\valof{y}| |\valof{x}|))
\end{lstlisting}
%
Dort ist der erste Teilausdruck unterstrichen, der beim ersten
Substitutionsschritt ersetzt wird.  Wenn die Programm-Funktion
\lstinline{+} tatsächlich die mathematische Operation $+$
realisiert,\footnote{Die Komplikationen durch inexakte Zahlen und
  Rundungen bleiben hier unberücksichtigt.}
wird der Teilausdruck \lstinline[mathescape]!(+ $\textnormal{\valof{x}}$ $\textnormal{\valof{y}}$)! durch $x+y$
ersetzt~-- beziehungsweise durch die Zahl, für die der mathematische
Ausdruck $x+y$ steht.  Es kommt also wieder \valof{\_} zum Einsatz:
%
\begin{lstlisting}
(= |\redex{(+ \valof{x} \valof{y})}| (+ |\valof{y}| |\valof{x}|))
$\Longrightarrow$ (= |\valof{x+y}| |\redex{(+ \valof{y} \valof{x})}|)
\end{lstlisting}
%
Entsprechend geht es weiter mit der zweiten Summe und schließlich der
Vergleichsoperation \lstinline{=}, die dem mathematischen $=$ entspricht:
%
\begin{lstlisting}
$\Longrightarrow$ |\redex{(= \valof{x+y} \valof{y+x})}|
$\Longrightarrow$ |\valof{x+y = y+x}|
$=$ #t
\end{lstlisting}
%
Die Kommutativität der Programm-Funktion \lstinline{+} folgt also aus der
Kommutativität des mathematischen $+$, durch das sie definiert ist.

\section{Rekursive Programme beweisen}
\label{sec:rek-scheme-beweisen}

Beweise über rekursive Programme sind anspruchsvoller als der
Beweis der Kommutativität von \lstinline{+}, benutzen aber die gleichen
Techniken sowie~-- genau wie bei Beweisen mathematischer rekursiver
Funktionen~-- Induktion als Beweisprinzip. 

\subsection{Rekursive Programme auf Listen}

Als erstes Beispiel dient
die Reflexivität.  Es gilt für die Bindung von \lstinline{lis} an eine
beliebige Liste von Zahlen folgendes zu beweisen:
%
\begin{lstlisting}
(number-list=? lis lis)
$\Longrightarrow\ldots\Longrightarrow$ #t
\end{lstlisting}
%
Wieder wird für den Wert der Bindung eine mathematische Variable
eingeführt~-- $l$.  Dann läuft der Beweis auf folgendes hinaus:
%
\begin{lstlisting}
(number-list=? lis lis)
$=$ (number-list=? |\valof{l}| |\valof{l}|)
$\Longrightarrow\ldots\Longrightarrow$ #t
\end{lstlisting}
%
\ldots~und dies ist zu beweisen für \emph{alle} Listen von Zahlen $l$.
Für diesen Beweis kommt uns die induktive Struktur der Listen zur
Hilfe, die der Struktur der endlichen Folgen~-- bekannt aus
Abschnitt~\ref{sec:finite-sequences} auf
Seite~\pageref{sec:finite-sequences}~-- entspricht.  Dazu müssen wir
zunächst einmal zwischen allen Fällen der gemischten
Datendefinition unterscheiden, also zwischen den leeren und den nichtleeren Listen.

\paragraph{Leere Liste}
Angenommen, $l$ ist die leere Liste.  Dann beginnt die Reduktion
folgendermaßen:
%
\begin{lstlisting}
(number-list=? |\valof{l}| |\valof{l}|)
$\Longrightarrow$ ((lambda (lis-1 lis-2) |\ldots|) |\valof{l}| |\valof{l}|)
$\Longrightarrow$ (cond ((empty? |\valof{l}|) |\ldots|) ((cons? |\valof{l}|) |\ldots|))
$\Longrightarrow$ (cond ((empty? |\valof{l}|) |\ldots|) ((cons? |\valof{l}|) |\ldots|))
$\Longrightarrow$ (cond (#t (cond |\ldots|)) ((cons? |\valof{l}|) #f))
$\Longrightarrow$ (cond ((empty? |\valof{l}|) #t) ((cons? |\valof{l}|) #f))
$\Longrightarrow$ (cond (#t #t) ((cons? |\valof{l}|) #f))
$\Longrightarrow$ #t
\end{lstlisting}
%

\paragraph{Nichtleere Liste}
Für diesen Fall stimmt die Behauptung also.  Angenommen, $l$ ist
\emph{nicht} die leere Liste, hat also erstes Element $f$ und Rest
$r$.  In diesem Fall können wir strukturelle Induktion benutzen.  Die
\emph{Induktionsvoraussetzung} bezieht sich dann auf den Rest $r$:
%
\begin{lstlisting}
(number-list=? |\valof{r}| |\valof{r}|)
$\Longrightarrow\ldots\Longrightarrow$ #t
\end{lstlisting}
%
Diese können wir benutzen.  Zunächst einmal müssen wir aber soweit
reduzieren wie möglich:
%
\begin{lstlisting}
(number-list=? |\valof{l}| |\valof{l}|)
$\Longrightarrow$ ((lambda (lis-1 lis-2) |\ldots|) |\valof{l}| |\valof{l}|)
$\Longrightarrow$ (cond ((empty? |\valof{l}|) |\ldots|) ((cons? |\valof{l}|) |\ldots|))
$\Longrightarrow$ (cond (#f |\ldots|) ((cons? |\valof{l}|) |\ldots|))
$\Longrightarrow$ (cond (#t (cond |\ldots|)))
$\Longrightarrow$ (cond ((empty? |\valof{l}|) |\ldots|) ((cons? |\valof{l}|) |\ldots|))
$\Longrightarrow$ (cond (#f |\ldots|) ((cons? |\valof{l}|) |\ldots|))
$\Longrightarrow$ (cond (#t (and |\ldots|)))
$\Longrightarrow$ (and (= (first |\valof{l}|) (first |\valof{l}|)) (number-list=? |\ldots|))
\end{lstlisting}
%
Da \lstinline{(first $\textnormal{\valof{l}}$)} das erste Element $f$ liefert, geht es
so weiter:
\begin{lstlisting}
$\Longrightarrow$ (and (= |\valof{f}| (first |\valof{l}|)) (number-list=? |\ldots|))
$\Longrightarrow$ (and (= |\valof{f}| |\valof{f}|) (number-list=? |\ldots|))
$\Longrightarrow$ (and #t (number-list=? |\ldots|))
$\Longrightarrow$ (number-list=? (rest |\valof{l}|) (rest |\valof{l}|))
\end{lstlisting}
%
Da \lstinline{(rest $\textnormal{\valof{l}}$)} den Rest $r$ liefert, geht es dann so
weiter:
%
\begin{lstlisting}
$\Longrightarrow$ (number-list=? |\valof{r}| (rest |\valof{l}|))
$\Longrightarrow$ (number-list=? |\valof{r}| |\valof{r}|)
\end{lstlisting}
%
Nach der Induktionsvoraussetzung wissen wir aber, dass der letzte
Ausdruck zu \lstinline{#t} reduziert wird.  Die Behauptung ist damit
bewisen.


\subsection{Rekursive Programme auf Zahlen}

Die Definition von \lstinline{factorial}\index{factorial@\texttt{factorial}} am Anfang von
Abschnitt~\ref{sec:factorial} folgt der induktiven Definition der
zugrundeliegenden Daten, der natürlichen Zahlen.  Dementsprechend ist
der Induktionsbeweis für dessen Korrektheit einfach.  Es ist aber
entscheidend, die zu beweisende Eigenschaft, welche die Korrektheit
von \lstinline{factorial} begründet, sorgfältig aufzuschreiben:

Die Funktion \lstinline{factorial} soll die Fakultät berechnen, es soll
also für alle natürlichen Zahlen $k$ gelten:
%
\begin{lstlisting}
(factorial |\valof{k}|)
$\Longrightarrow\ldots\Longrightarrow$ |\valof{k!}|
\end{lstlisting}
%
(Diese Eigenschaft lässt sich nicht sinnvoll mit \lstinline{for-all}
hinschreiben, da die mathematische Fakultät nicht fest eingebaut ist.)

Da es um natürliche Zahlen geht, ist vollständige Induktion
anwendbar.  Wir verwenden das Schema aus
Abschnitt~\ref{sec:nat-induction-ka} auf
Seite~\pageref{sec:nat-induction-ka}:
%
\begin{enumerate}
\item Die Behauptung ist bereits in der geforderten Form.
\item $k = 0$:
\begin{lstlisting}
(factorial 0)
$\Longrightarrow$ |\valof{0!}|
\end{lstlisting}
%
\item Beweis für $k=0$:
\begin{lstlisting}
(factorial 0)
$\Longrightarrow$ ((lambda (n) |\ldots|) 0)
$\Longrightarrow$ (if (= 0 0) |\ldots|)
$\Longrightarrow$ (if #t 1 |\ldots|)
$\Longrightarrow$ 1
$=$ |\valof{0!}|
\end{lstlisting}
%
\item Induktionsvoraussetzung:

\begin{lstlisting}
(factorial |\valof{k}|)
$\Longrightarrow\ldots\Longrightarrow$ |\valof{k!}|
\end{lstlisting}

\item Induktionsschluss (zu zeigen):

\begin{lstlisting}
(factorial |\valof{k+1}|)
$\Longrightarrow\ldots\Longrightarrow$ |\valof{(k+1)!}|
\end{lstlisting}
\item 

Der Beweis sieht so aus:
%
\begin{lstlisting}
(factorial |\valof{k+1}|)
$\Longrightarrow$ ((lambda (n) |\ldots|) |\valof{k+1}|)
$\Longrightarrow$ (if (= |\valof{k+1}| 0) |\ldots|)
$\Longrightarrow$ (if #f 1 (* |\ldots|))
$\Longrightarrow$ (* |\valof{k+1}| (factorial (- |\valof{k+1}| 1)))
$\Longrightarrow$ (* |\valof{k+1}| (factorial |\valof{k}|))
$=$ (* |\valof{k+1}| (factorial |\valof{k}|))
\end{lstlisting}
%
Mit der Induktionsannahme kann \lstinline{(factorial $\textnormal{\valof{k}}$)} ersetzt werden:
%
\begin{lstlisting}
(* |\valof{k}| (factorial |\valof{l}|))
$\Longrightarrow\ldots\Longrightarrow$ (* |\valof{k+1}| |\valof{k!}|)
$\Longrightarrow$ |\valof{(k+1) \times k!}|
$=$ |\valof{(k+1)!}|
\end{lstlisting}
%
\end{enumerate}

Damit ist der Beweis fertig.

Die Technik funktioniert auch mit Beispielen, bei denen die zu
beweisende Eigenschaft nicht so einfach zu sehen ist wie bei
\lstinline{factorial}.

Die folgende Funktion verrät nicht auf den ersten Blick, was
sie berechnet:
%
\begin{lstlisting}
(: f (natural -> rational))

(define f
  (lambda (n)
    (if (= n 0)
        0
        (+ (f (- n 1))
           (/ 1 (* n (+ n 1)))))))
\end{lstlisting}
%
Tatsächlich berechnet der Funktionaufruf \lstinline{(f $\textnormal{\valof{k}}$)} für
eine natürliche Zahl $k$ die Zahl
$\frac{k}{k+1}$.

Die Eigenschaft ist plausibel, wie sich mit \lstinline{check-property}
feststellen lässt:
%
\begin{lstlisting}
(check-property
 (for-all ((k natural))
   (= (f k) (/ k (+ k 1)))))
\end{lstlisting}
%
Ein Beweis schafft Sicherheit.  Wieder gehen wir nach dem bekannten
Schema vor:
%
\begin{enumerate}
\item Behauptung:

  Für alle $k\in\mathbb{N}$ gilt:

\begin{lstlisting}
(f |\valof{k}|)
$\Longrightarrow\ldots\Longrightarrow$ |\valof{\frac{k}{k+1}}|
\end{lstlisting}

\item $k=0$:
%
\begin{lstlisting}
(f |\valof{0}|)
$\Longrightarrow$|\ldots|$\Longrightarrow$ |\valof{\frac{0}{0+1}}|
\end{lstlisting}

\item Beweis:
\begin{lstlisting}
(f |\valof{0}|)
$\Longrightarrow$ ((lambda (n) |\ldots|) 0)
$\Longrightarrow$ (if (= 0 0) 0 |\ldots|)
$\Longrightarrow$ (if #t 0 |\ldots|)
$\Longrightarrow$ 0
$=$ |\valof{\frac{0}{0+1}}|
\end{lstlisting}
%
\item Induktionsvoraussetzung:

\begin{lstlisting}
(f |\valof{k}|)
$\Longrightarrow\ldots\Longrightarrow$ |\valof{\frac{k}{k+1}}|
\end{lstlisting}

\item
Induktionsschluss (zu zeigen):
%
\begin{lstlisting}
(f |\valof{k+1}|)
$\Longrightarrow\ldots\Longrightarrow$ |\valof{\frac{k+1}{(k+1)+1}}|
\end{lstlisting}
%
\item Beweis:
\begin{lstlisting}
(f |\valof{k+1}|)
$\Longrightarrow$ ((lambda (n) (if |\ldots|)) |\valof{k+1}|)
$\Longrightarrow$ (if (= |\valof{k+1}| 0) |\ldots|)
$\Longrightarrow$ (if #f |\ldots| (+ |\ldots|))
$\Longrightarrow$ (+ (f (- |\valof{k+1}| 1)) (/ 1 (* |\valof{k+1}| (+ |\valof{k+1}| 1))))
$\Longrightarrow$ (+ (f |\valof{k}|) (/ 1 (* |\valof{k+1}| (+ |\valof{k+1}| 1))))
$\Longrightarrow\ldots\Longrightarrow$ (+ |\valof{\frac{k}{k+1}}| (/ 1 (* |\valof{k+1}| (+ |\valof{k+1}| 1))))
$\Longrightarrow$ (+ |\valof{\frac{k}{k+1}}| (/ 1 (* |\valof{k+1}| |\valof{(k+1)+1}|)))
$\Longrightarrow$ (+ |\valof{\frac{k}{k+1}}| (/ 1 |\valof{(k+1)\times((k+1)+1)}|))
$\Longrightarrow$ (+ |\valof{\frac{k}{k+1}}| |\valof{\frac{1}{(k+1)\times((k+1)+1)}}|)
$\Longrightarrow$ |\valof{\frac{k}{k+1} + \frac{1}{(k+1)\times((k+1)+1)}}|
$=$ |\valof{\frac{k}{k+1} + \frac{1}{(k+1)\times(k+2)}}|
$=$ |\valof{\frac{k\times(k+2) + 1}{(k+1)\times(k+2)}}|
$=$ |\valof{\frac{k\sp{2} + 2k + 1}{(k+1)\times(k+2)}}|
$=$ |\valof{\frac{(k+1)\sp{2}}{(k+1)\times(k+2)}}|
$=$ |\valof{\frac{k+1}{k+2}}|
$=$ |\valof{\frac{k+1}{(k+1)+1}}|
\end{lstlisting}
%
\end{enumerate}
Damit ist die Behauptung bewiesen.

% Das gleiche Spiel lässt sich auch am Beispiel der Funktion \lstinline{f}
% aus Abschnitt~\ref{sec:rek-scheme-beweisen} demonstrieren.  Eine
% iterative Variante von \lstinline{f} ist:
% %
% \begin{alltt}
% (define f
%   (lambda (n)
%     (f-helper n 0)))

% (define f-helper
%   (lambda (n result)
%     (if (= n 0)
%         result
%         (f-helper (- n 1)
%                   (+ (/ 1 (* n (+ n 1)))
%                      result)))))
% \end{alltt}
% %
% Zur Erinnerung: \lstinline{(f $n$)} liefert $\frac{n}{n+1}$.

\section{Invarianten}
\label{sec:invarianten}

Die bisher angewendete Technik für den Beweis rekursiver Funktionen
mit Induktion funktioniert bei Funktionen mit Akkumulator nicht mehr
direkt: Angenommen, die Korrektheit der endrekursiven Fakuktät
\lstinline{!} aus Abschnitt~\ref{page:factorial-tail} soll ähnlich die
die Korrektheit von \lstinline{factorial} bewiesen werden.  Wieder sei
\lstinline{n} an eine natürliche Zahl $k$ gebunden:
%
\begin{lstlisting}
(! n)
$=$ (! |\valof{k}|)
$\Longrightarrow$ ((lambda (n) (!-helper n 1)) |\valof{k}|)
$\Longrightarrow$ (!-helper |\valof{k}| 1)
$\Longrightarrow$ ((lambda (n acc) |\ldots|) |\valof{k}| 1)
$\Longrightarrow$ (if (= |\valof{k}| 0) 1 (!-helper (- |\valof{k}| 1) (* 1 |\valof{k}|)))
\end{lstlisting}
%
Wie bei \lstinline{factorial} muss zwischen $k=0$ und $k>0$ unterschieden
werden.  Für $k=0$ geht es folgendermaßen weiter:
%
\begin{lstlisting}
$\Longrightarrow$ (if (= |\valof{k}| 0) 1 (!-helper (- |\valof{k}| 1) (* 1 |\valof{k}|)))
$\Longrightarrow$ (if #t 1 (!-helper (- |\valof{k}| 1) (* 1 |\valof{k}|)))
$\Longrightarrow$ 1
\end{lstlisting}
%
Für $k=0$ funktioniert also der Beweis.  Für $k>0$ allerdings verläuft
die Reduktion folgendermaßen:
%
\begin{lstlisting}
$\Longrightarrow$ (if (= |\valof{k}| 0) 1 (!-helper (- |\valof{k}| 1) (* 1 |\valof{k}|)))
$\Longrightarrow$ (if #f 1 (!-helper (- |\valof{k}| 1) (* 1 |\valof{k}|)))
$\Longrightarrow$ (!-helper (- |\valof{k}| 1) (* 1 |\valof{k}|))
\end{lstlisting}
%
Hier gibt es zwar einen rekursiven Aufruf mit Argument
\lstinline{(- $\textnormal{\valof{k}}$ 1)}, aber \emph{der Akkumulator hat sich auch verändert.}
Damit ist die naheliegende Induktionsannahme für
\lstinline{(!-helper (- $\textnormal{\valof{k}}$ 1) $\textnormal{\valof{a}}$)} (falls der Wert des Akkumulators
\lstinline{acc} $a$ ist) wertlos.  Funktionen mit Akkumulator sind also
nicht nur schwieriger zu schreiben als "<regulär"> rekursive
Funktionen~-- sie sind auch schwerer zu beweisen.

Stattdessen ist es bei Funktionen mit Akkumulator nützlich, eine
\textit{Invariante\index{Invariante}} aufzustellen, also eine
Eigenschaft, welche Zwischenergebnis und noch zu leistende Arbeit in
Beziehung setzt.  Wie in Abschnitt~\ref{page:factorial-tail}
beschrieben, geht die Fakultätsfunktion mit Akkumulator folgendermaßen
vor, um \lstinline{(! 4)} auszurechnen:
%
\begin{displaymath}
  (((1 \times 4)\times 3)\times 2)\times 1
\end{displaymath}
%
Bei jedem rekursiven Aufruf lässt sich dieser Aufruf in "<geleistete
Arbeit"> (die durch den Akkumulator repräsentiert ist) und "<noch zu
leistende Arbeit"> unterteilen.  Zum Beispiel entsteht ein rekursiver
Aufruf \lstinline{(!-helper 2 12)}, bei der Akkumulator der Wert des
unterstrichenen Teilaufrufs ist:
%
\begin{displaymath}
  (\underline{((1 \times 4)\times 3)}\times 2)\times 1
\end{displaymath}
%
Es ist zu sehen, dass die noch zu leistende Arbeit gerade darin
besteht, den Akkumulator noch mit der Fakultät von 2 zu
multiplizieren.  Wenn bei einem rekursiven Aufruf von \lstinline{!-helper} der
Wert von \lstinline{n} $k$ ist und der Wert des Akkumulators $a$, und am
Ende die Fakultät von $N$ berechnet werden soll, dann gilt bei jedem
rekursiven Aufruf \lstinline{(!-helper $\textnormal{\valof{n}}$ $\textnormal{\valof{a}}$)} immer:
%
\begin{displaymath}
  a \times k! = N!
\end{displaymath}
%
Dies ist die Invariante von \lstinline{!-helper} und heißt so, weil sie beim
rekursiven Aufruf von \lstinline{!-helper} unverändert bleibt.  Dies
ist zunächst nur eine Behauptung, aber wenn sie gelten sollte, dann
folgt daraus automatisch die Korrektheit der Funktion, da bei $k=0$
gilt:
%
\begin{displaymath}
  a \times 0! = a \times 1 = a = N!
\end{displaymath}
%
Dass $a \times k! = N!$ tatsächlich die Invariante ist, lässt sich
folgendermaßen folgern:
%
\begin{itemize}
\item Sie gilt für den ersten Aufruf von \lstinline{!-helper} von
  \lstinline{!}, da dort $k=N$ und $a=1$ gilt, also:
  \begin{displaymath}
    a \times k! = 1 \times N! = N!
  \end{displaymath}
\item Jeder rekursive Aufruf erhält die Invariante.  Angenommen, sie
  gilt für $k$ und $a$, dann sind die neuen Werte für $k$ und $a$ im
  rekursiven Aufruf \lstinline{(!-helper (- $\textnormal{\valof{n}}$ 1) (* $\textnormal{\valof{a}}$ $\textnormal{\valof{k}}$))} gerade
  $k\mapsto k-1$ und $a \mapsto a\times n$, die Invariante wäre also:
  \begin{eqnarray*}
    (a \times k) \times (k-1)! &=& a \times (k \times (k-1)!\\
    &=& a\times k!\\
    &=& N!
  \end{eqnarray*}
\end{itemize}
%
Diese Technik funktioniert auch bei weniger offensichtlichen
Funktionen.  Hier eine Funktion, die äquivalent ist zu der Funktion
\lstinline{f} aus Abschnitt~\ref{sec:rek-scheme-beweisen}:

\begin{lstlisting}
; n/(n+1) berechnen
(: f (natural -> natural))

(define f
  (lambda (n)
    (f-helper n 0)))

(define f-helper
  (lambda (n acc)
    (if (= n 0)
        acc
        (f-helper (- n 1)
                  (+ (/ 1 (* n (+ n 1)))
                     acc)))))
\end{lstlisting}
%
Die Funktion geht folgendermaßen vor, um das Ergebnis für eine Eingabe
$n$ zu berechnen:
%
\begin{displaymath}
  (\ldots ((\frac{1}{n \times (n + 1)}
  + \frac{1}{(n - 1) \times ((n - 1) + 1)})
  + \frac{1}{(n - 2) \times ((n - 2) + 1)})
  + \ldots
  + \frac{1}{1 \times (1 + 1)})
\end{displaymath}
%
Diese Summe ist bei jedem rekursiven Aufruf aufgeteilt als Summe von
zwei Teilen, z.B.\ wie folgt:
%
\begin{displaymath}
  (\ldots \underline{((\frac{1}{n \times (n + 1)}
  + \frac{1}{(n - 1) \times ((n - 1) + 1)})
  + \frac{1}{(n - 2) \times ((n - 2) + 1)})}
  + \ldots
  + \frac{1}{1 \times (1 + 1)})
\end{displaymath}
%
Der unterstrichene Teil ist gerade der Wert des Akkumulators, die
Summe rechts davon der noch zu berechnende Summand.  
Wenn die Funktion tatsächlich $n/(n+1)$ berechnen sollte, ist dieser
rechte Teil im Beispiel $(n-3)/((n-3)+1)$.  Damit ergibt
sich die Invariante als $a + n/(n+1)$, wobei $a$ der Wert von
\lstinline{acc} ist.  Um die Annahme zu beweisen, dass dies die Invariante
ist, muss im wesentlichen folgende Gleichung bewiesen werden:
\[a+ \frac{n}{n+1} = a + \frac{n-1}{n} + \frac{1}{n\times (n+1)}\]
Dies ist eine lohnende Fingerübung.

\section{Korrektheit von Suchbäumen beweisen}

FIXME

Die beiden \texttt{check-property}-Tests stärken also das Vertrauen in
die korrekte Funktionsweise von \texttt{search-tree-insert} und
\texttt{search-tree-member?}.  Aber auch hier ist Kontrolle über einen
Beweis der Korrektheit noch besser:
Es lohnt sich, etwas formaler über die
Korrektheit von \texttt{search-tree-insert} nachzudenken.  Zunächst
einmal ist es wichtig, zu formulieren, was der Begriff "<Korrektheit">
im Zusammenhang mit \texttt{search-tree-insert} überhaupt bedeutet:
%
\begin{satz}\label{satz:suchbaum}
  \texttt{Search-tree-insert} \emph{erhält die Suchbaumeigenschaft}.
  Oder mit anderen Worten: Wenn das \texttt{search-tree}-Argument von
  \texttt{search"=tree"=insert} die Suchbaumeigenschaft erfüllt, so
  erfüllt auch der zurückgegebene Baum die Suchbaumeigenschaft\index{Suchbaumeigenschaft}.
\end{satz}
%
\begin{beweis}
  Die Korrektheit ist an der Hilfsfunk tion \texttt{insert}
  festgemacht: Wenn das Argument von \texttt{insert} die
  Suchbaumeigenschaft erfüllt, so muss auch der Rückgabewert sie
  erfüllen.  Der Beweis funktioniert über strukturelle Induktion über
  den Wert \texttt{t}, der an den Baum $\tau$ gebunden sei.  Im
  Beweis gibt es vier Fälle, die den Zweigen der \texttt{cond}-Formen
  entsprechen:
%
\begin{itemize}
\item $\tau$ ist der leere Baum.  Der dann zurückgegebene Baum
  der Form

  TBD
  
% \begin{pspdf}
%   \begin{center}
%     \pstree[levelsep=4ex,treesep=3em,nodesep=2pt]{\Tr{$l$}}
%     {\Tdot\Tdot}
%   \end{center}
% \end{pspdf}
erfüllt offensichtlich die Suchbaumeigenschaft.
\item $\tau$ ist ein Knoten, dessen Markierung mit
  $l$ übereinstimmt.  Dann gibt \texttt{insert} 
  $\tau$ zurück.  Da $\tau$ nach Voraussetzung die
  Suchbaumeigenschaft erfüllt, ist auch hier die
  Suchbaumeigenschaft erhalten.
\item $\tau$ ist ein Knoten, dessen Markierung \emph{größer}
  ist als $l$, sieht also so aus:
% \begin{pspdf}
%   \begin{center}
%     \pstree[levelsep=4ex,treesep=3em,dotsize=0pt 0.1]{\Tr{$m$}}
%     {
%       \pstree{\Tdot}{\Ttri{\raisebox{-1ex}[0pt][1.8ex]{$a$}}}
%       \pstree{\Tdot}{\Ttri{\raisebox{-1ex}[0pt][1.8ex]{$b$}}}
%       }
%   \end{center}
% \end{pspdf}

  TBD
  
  wobei sowohl $a$ als auch $b$ selbst die Suchbaumeigenschaft
  erfüllen. In diesem
  Fall sieht der entstehende Baum folgendermaßen aus:
  %
  % \begin{pspdf}
  % \begin{center}
  %   \pstree[levelsep=4ex,treesep=3em,dotsize=0pt 0.1]{\Tr{$m$}} {
  %     \pstree{\Tdot}{\Ttri{\raisebox{-1ex}[0pt][1.8ex]{
  %         \texttt{(insert \valof{a})}
  %         }}}
  %     \pstree{\Tdot}{\Ttri{\raisebox{-1ex}[0pt][1.8ex]{$b$}}} }
  % \end{center}
  % \end{pspdf}

  TBD
  
% 
  Per Induktionsannahme erfüllt \texttt{(insert \valof{a})} die
  Suchbaumeigenschaft.  Da $b$ auch die Suchbaumeigenschaft
  erfüllt, muss nur noch gezeigt werden, dass alle Markierungen in
  \texttt{(insert \valof{a})} kleiner sind als $m$.
  Es gibt in \texttt{insert} drei Aufrufe von \texttt{make-node},
  die neue Knoten erzeugen können.  Alle fügen höchstens
  \texttt{l} zu der Menge der Markierungen des Baumes hinzu.
  Alle anderen Markierungen sind nach Voraussetzung kleiner als $m$,
  ebenso wie \texttt{l}.  Das Resultat erfüllt also ebenfalls
  die Suchbaumeigenschaft.
\item Im vierten Fall ist $\tau$ ein Knoten, dessen Markierung
  \emph{kleiner} ist als $l$.  Dieser Fall geht analog zum
  dritten Fall.
\end{itemize}
\end{beweis}


\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 sowohl der Ihnen bekannten arithmetischen Operationen
  als auch der 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üfen, ob \drscheme{} jeweils ein Gegenbeispiel
  findet.
\end{aufgabe}

\begin{aufgabe}
  \label{aufgabe:boolean-distrib}
  Für \lstinline{and} und \lstinline{or} gelten zwei Distributivgesetze
  analog dem Distributivgesetz für \lstinline{*} und \lstinline{+}:
  Formuliere diese als Eigenschaften und lasse sie \drscheme{}
  sie überprüfen.

  Abstrahiere dann über die nun insgesamt drei Distributivgesetze
  analog zu \lstinline{commutativity} und \lstinline{associativity} und
  formuliere die drei Distributivgesetze mit Hilfe der
  Abstraktion neu.  Schreibe eine möglichst aussagekräftige
  Signatur für Deine Abstraktion!
\end{aufgabe}

\begin{aufgabe}  Schreibe Abstraktionen analog zu \lstinline{commutativity} und
  \lstinline{associativity} für folgende Eigenschaften:
  \begin{enumerate}
  \item DeMorgan
  \item Reflexivität
  \item Symmetrie
  \item Antisymmetrie
  \item Transitivität
  \item linksneutrales Element
  \item rechtsneutrales Element
  \item inverses Element
  \end{enumerate}
\end{aufgabe}


\begin{aufgabe}
  Versuche, die Eigenschafts-Tests für \lstinline{number-list=?}
  auszutricksen, also eine fehlerhafte Version von
  \lstinline{number-list=?} zu schreiben, die alle drei
  \lstinline{check-property}-Tests besteht.
  Die \lstinline{check-expect}-Tests sind für diese Aufgabe nicht relevant.
\end{aufgabe}

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

\begin{aufgabe}
  Finde eine präzisere Formulierung der Kommutativität von
  \lstinline{list-sum} als die in
  Abschnitt~\ref{sec:list-sum-commutative}, also eine, an der sich die
  Eigenschaft, dass die "<Reihenfolge der Elemente der Liste keine
  Rolle spielt"> klarer zu sehen ist.

  Schreibe dazu eine Funktion, welche die Reihenfolge der
  Elemente einer Liste abhängig von einer natürlichen Zahl $n$
  verändert, zum Beispiel indem die $n$te Permutation der Elemente ausgewählt
  wird.
\end{aufgabe}

\begin{aufgabe}
  Schreibe einen \lstinline{check-property}-Test für folgende Eigenschaft:
  \begin{center}
    \texttt{(uncurry (curry $p_2$))} $\equiv$ $p_2$
  \end{center}
\end{aufgabe}

\begin{aufgabe}
  Formuliere sinnvolle Eigenschaften von \lstinline{compose} und
  \lstinline{repeat} von Seite~\ref{page:repeat} und überprüfe
  diese mit \lstinline{check-property}!
\end{aufgabe}

\begin{aufgabe}
  Beweise, dass für Funktionen $p_1$ mit einem Parameter, die
  einparametrige Funktionen zurückgeben, und Funktionen $p_2$ mit zwei
  Parametern gilt:
  %
  \begin{center}
    \texttt{(curry (uncurry $p_1$))} $\equiv$ $p_1$\\
    \texttt{(uncurry (curry $p_2$))} $\equiv$ $p_2$
  \end{center}
\end{aufgabe}

\begin{aufgabe}
  Beweise die entsprechend dem Beweis der Kommutativität von
  \lstinline{+} in Abschnitt~\ref{sec:scheme-arithmetik-beweis} die
  Assoziativität von \lstinline{+} sowie die Distributivität von
  \lstinline{+} und \lstinline{*} aus
  Abschnitt~\ref{sec:eigenschaften-binaere-operationen}.
\end{aufgabe}

\begin{aufgabe}
Beweise, dass die
folgende Funktion natürliche Zahlen quadriert:
%
\begin{lstlisting}
; Quadrat einer Zahl berechnen
(: square (natural -> natural))
(define square
  (lambda (n)
    (if (= n 0)
        0
        (+ (square (- n 1))
           (- (+ n n) 1)))))
\end{lstlisting}
%
Formuliere dazu auch eine Eigenschaft und überprüfe diese
mit \lstinline{check-property}.
%
\end{aufgabe}

\begin{aufgabe}
Beweise, dass auch die folgende Funktion \lstinline{square}
natürliche Zahlen quadriert.  Gib die Invariante von
\lstinline{square-helper} an!
%
\begin{lstlisting}
; Quadrat einer Zahl berechnen
(: square (natural -> natural))
(define square
  (lambda (n)
    (square-helper n 0)))

(define square-helper
  (lambda (n acc)
    (if (= n 0)
        acc
        (square-helper (- n 1)
                       (+ acc
                          (- (+ n n) 1))))))
\end{lstlisting}
Formuliere dazu auch eine Eigenschaft und überprüfe diese
mit \lstinline{check-property}.
\end{aufgabe}

\begin{aufgabe}
 Beweise mit Hilfe des Substitutionsmodells, dass
  die \lstinline{concatenate}-Funktion aus Abschnitt~\ref{sec:lists}
  assoziativ ist, dass also für Listen $l_1$, $l_2$ und $l_3$ gilt:
\begin{lstlisting}
(concatenate $l\sb{1}$ (concatenate $l\sb{2}$ $l\sb{3}$)) $=$ (concatenate (concatenate $l\sb{1}$ $l\sb{2}$) $l\sb{3}$)
\end{lstlisting}

  \begin{aufgabe}
    Beweise die Korrektheit von \texttt{search-tree-member?} in
    Abschnitt~\ref{func:search-tree-member} auf Seite
    \pageref{func:search-tree-member}.  Formuliere zunächst eine
    geeignete Korrektheitseigenschaft und beweisen diese mit Hilfe
    von Induktion!
\end{aufgabe}

\begin{aufgabe}
  Falls Du Aufgabe~\ref{aufgabe:search-tree-delete} auf
  Seite~\pageref{aufgabe:search-tree-delete} gelöst hast
  (\lstinline{search-tree-delete}): Beweisen, dass die Funktion die
  Suchbaumeigenschaft erhält.
\end{aufgabe}
\end{aufgabe}


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