Warum Tests nicht genügen

Ein Test prüft ein Programm an einigen Eingaben, ein Beweis prüft es an allen. Das ist der Unterschied zwischen „bei mir hat es funktioniert“ und „es funktioniert immer“.

Ein Verkehrsbetrieb testet seinen Fahrkartenautomaten mit drei Fahrgästen: acht, dreißig und siebzig Jahre alt. Alle drei Tests sind grün. Trotzdem zahlen Vierzehnjährige und Fünfundsechzigjährige den falschen Preis.

Ein Test ist ein Beispiel. Er zeigt: Für diese Eingabe stimmt die Ausgabe. Über alle anderen Eingaben sagt er nichts.

Die Regel, an die sich der Automat halten soll, heißt Spezifikation. Ein Test vergleicht die Ausgabe des Programms mit der Spezifikation, aber nur für die Eingaben, die jemand aufgeschrieben hat.

def soll(alter):
    # Die Regel: bis 14 Jahre 150 Cent, bis 64 Jahre 300 Cent, ab 65 Jahren 200 Cent.
    if alter <= 14:
        return 150
    if alter <= 64:
        return 300
    return 200


def automat(alter):
    # Der Automat vergleicht an zwei Stellen falsch.
    if alter < 14:
        return 150
    if alter <= 65:
        return 300
    return 200


getestet = [8, 30, 70]
for alter in getestet:
    print(alter, soll(alter) == automat(alter))
# Fuegen Sie 14 zu getestet hinzu und fuehren Sie erneut aus.

Ein Alter ist eine ganze Zahl von 0 bis 120. Das sind nur 121 Fälle. Prüft ein Programm alle 121, ist das ein Beweis, denn es gibt keinen anderen Fall mehr.

Ist der Eingabebereich klein genug, darf ein Test also alles prüfen. Das heißt erschöpfendes Testen. Der Befehl unten tut das für die zwei Schreibweisen der Altersgrenze und nennt jedes Alter, bei dem sie sich unterscheiden.

python3 -c "print([a for a in range(0, 121) if (a < 14) != (a <= 14)])"

Eine Zahl aus 32 Bit hat 2 hoch 32 mögliche Werte. Der erste Befehl zeigt, wie viele das sind.

Der zweite rechnet aus, wie viele Jahre ein Rechner braucht, der eine Milliarde Fälle in der Sekunde prüft. Die Eingabe besteht dabei aus zwei solchen Zahlen, das sind 2 hoch 64 Fälle. Ein Jahr hat hier 365 Tage, das Ergebnis ist abgerundet.

python3 -c "print(2 ** 32)"

python3 -c "print(2 ** 64 // (10 ** 9 * 3600 * 24 * 365))"

Eine formale Methode nutzt Mathematik statt Ausprobieren: Ein Rechner entscheidet, ob eine Regel für alle Eingaben gilt, oder nennt ein Gegenbeispiel.

Das Werkzeug heißt Z3. Die nächste Lektion erklärt es genauer. Hier sehen Sie nur, was es kann: Gibt es eine 32-Bit-Zahl x mit Vorzeichen, die kleiner wird, wenn man 1 addiert? Z3 antwortet sat, es gibt eine, und nennt sie. #x7fffffff ist die größte solche Zahl, 2147483647, in Hexadezimalschreibweise.

printf '(declare-const x (_ BitVec 32))\n(assert (bvslt (bvadd x #x00000001) x))\n(check-sat)\n(get-value (x))\n' | z3 -in

Schreiben Sie die Regel für einen eigenen Automaten, etwa für den Preis einer Bibliotheksmahnung nach Tagen. Bauen Sie absichtlich einen Fehler an einer Grenze ein und suchen Sie ihn mit möglichst wenigen Tests.

Überlegen Sie, an welchen Stellen eines Bereichs Fehler am häufigsten stecken, und warum Grenzwerte gute Testfälle sind.