Folgende Routine berechnet in der Variablen \(y\) die Fibonacci-Zahl \(\mathop{\mathrm{fib}}(n)\) für \(n \geq 0\):
y := 0;
x := 1;
i := 0;
while (i < n) {
aux := y;
y := x;
x := x + aux;
i := i + 1;
}
Zeigen sie, dass dem wirklich so ist:
1. Formulieren sie zunächst die Spezifikation als Vor- und Nachbedingung. Tragen sie diese oben in die erste bzw. letzte Zeile ein.
2. Finden sie nun eine geeignete Invariante:
Die Invariante besagt informell unter anderem, dass \(y\) die \(i\)-te und \(x\) die \(i+1\)-te Fibonaccizahl ist.
3. Berechnen Sie rückwärts die (laufenden) Vorbedingungen, indem Sie diese im Code annotieren.
4. Berechnen Sie zuerst die drei resultierenden Beweisverpflichtungen explizit in den folgenden Feldern, und beweisen Sie diese dann in den Zeilen darunter.
Hinweis: Für den Beweis können Sie annehmen, dass \(\mathop{\mathrm{fib}}(n)\) wie folgt definiert ist:
Es werden keine Daten übertragen. Per Klick auf "Ergebnis speichern" kann eine Datei gespeichert werden, welche die eingegebenen Ergebnisse enthält. Diese Datei sendet ihr bitte rechtzeitig bis Dienstag 23:59:59 an martin (punkt) ring (klammeraffe) dfki (punkt) de. Ihr könnt eure Abgabe später auch wieder laden und ansehen indem ihr auf "Ergebnis laden" klickt.
