Schleifeninvariante

Grundidee der Schleifeninvariante

Eine Schleifeninvariante ist in der Informatik eine besondere Form einer Invariante. Sie ist ein logischer Ausdruck, der am Anfang und am Ende jedes Schleifendurchlaufs sowie vor und nach der Ausführung der Schleife gültig ist. Ihre Gültigkeit hängt daher nicht von der aktuellen Anzahl der Durchläufe ab. Ein solcher Ausdruck kann wahr oder falsch sein.

Schleifeninvarianten werden vor allem zur formalen Verifizierung von Algorithmen verwendet. Sie helfen außerdem dabei, die Vorgänge innerhalb einer Schleife genauer zu erfassen. Typischerweise beschreiben sie Wertebereiche von Variablen oder Beziehungen zwischen mehreren Variablen.

Zu jeder Schleife kann grundsätzlich eine Invariante gefunden werden, etwa die stets wahre Tautologie „wahr = wahr“. Eine solche Invariante ist jedoch nicht unbedingt geeignet, einen formalen Korrektheitsbeweis zu führen. Dafür muss sie die für den Algorithmus wichtigen Eigenschaften ausdrücken.

Nachweis der Schleifenkorrektheit

Nach dem Hoare-Kalkül muss beim Beweis einer Schleife mithilfe einer Schleifeninvariante gezeigt werden, dass die Invariante direkt vor der Ausführung der Schleife und nach jeder Prüfung der Schleifenbedingung gilt. Nach dieser Prüfung gibt es zwei Möglichkeiten: Ist die Schleifenbedingung erfüllt, wird ein weiterer Durchlauf begonnen; ist sie nicht erfüllt, wird die Schleife verlassen.

Deshalb muss die Invariante sowohl direkt am Anfang jedes Schleifendurchlaufs als auch unmittelbar nach der Schleife gelten. Der Beweis untersucht insbesondere, ob die Invariante beim Eintritt in die Schleife gilt, während eines Durchlaufs erhalten bleibt und beim Verlassen der Schleife noch gültig ist.

Partielle Korrektheit

Für den Nachweis der partiellen Korrektheit werden drei Zeitpunkte betrachtet:

• Zuerst wird geprüft, ob die Invariante direkt vor der Schleife gilt. Dies ist der erste kritische Zeitpunkt.
• Danach wird geprüft, ob sie beim Übergang von einem Schleifendurchlauf zum nächsten erhalten bleibt.
• Schließlich muss die Invariante auch direkt nach der Schleife gelten.

Dieses Vorgehen entspricht der vollständigen Induktion in der Mathematik. Zu allen drei Zeitpunkten müssen die von der Invariante behaupteten Eigenschaften korrekt sein, zum Beispiel dass Variablen in bestimmten Wertebereichen liegen oder bestimmte Beziehungen zueinander erfüllen.

Nach dem Verlassen der Schleife gelten die Invariante und außerdem die abweisende Schleifenbedingung, also die Bedingung, die beim Verlassen nicht erfüllt ist. Wenn sich aus der Und-Verknüpfung dieser beiden Aussagen das gewünschte Ergebnis der Schleife ergibt, ist ihre partielle Korrektheit bewiesen.

Partielle Korrektheit bedeutet: Immer wenn die Schleife terminiert, also verlassen wird, liegt das korrekte Ergebnis vor. Damit ist jedoch noch nicht bewiesen, dass die Schleife tatsächlich immer terminiert.

Totale Korrektheit und Terminierung

Für die totale Korrektheit muss zunächst die partielle Korrektheit nachgewiesen werden. Zusätzlich muss bewiesen werden, dass die Schleife in jedem Fall terminiert.

Dazu wird zunächst bestimmt, unter welchen Bedingungen die Schleife verlassen werden kann. Anschließend muss gezeigt werden, dass diese Bedingungen tatsächlich in jedem Fall erreicht werden. Ein Beispiel ist die Zählervariable einer For-Schleife: Sie erhöht sich bei jedem Durchlauf bis zu einer Obergrenze und wird innerhalb der Schleife nicht verändert. Dadurch wird sichergestellt, dass die Abbruchbedingung erreicht wird.

Sind sowohl die Terminierung als auch das anschließende Vorliegen des gewünschten Ergebnisses bewiesen, ist die totale Korrektheit der Schleife nachgewiesen. Außerdem ist bewiesen, dass es keinen Algorithmus gibt, der für alle Schleifen automatisch eine Schleifeninvariante findet, die sich für einen Korrektheitsbeweis verwenden lässt.

Beispiel: Multiplikation durch wiederholtes Addieren

Der dargestellte Algorithmus multipliziert die Variablen a und b, indem er wiederholt addiert. Zu Beginn werden x auf a, y auf b und p auf 0 gesetzt. Danach läuft die Schleife, solange x > 0 gilt:

• p wird um y erhöht: p := p + y.
• x wird um 1 verringert: x := x - 1.

Eine passende Schleifeninvariante lautet:

(x · y) + p = a · b

Sie gilt vor der Schleife, am Anfang jedes Durchlaufs, am Ende jedes Durchlaufs und direkt nach der Schleife. Innerhalb des Schleifenkörpers muss sie dagegen nicht zu jedem Zeitpunkt gelten. Insbesondere ist sie direkt nach der Anweisung p := p + y zunächst nicht erfüllt; nach der anschließenden Verringerung von x gilt sie wieder.

Wenn die Schleife endet, ist x nicht mehr größer als 0. Da x bei jedem Durchlauf um 1 verringert wird, gilt am Ende x = 0. Zusammen mit der Invariante folgt dann p = a · b. Der zurückgegebene Wert p ist somit das gewünschte Produkt.

Native Unterstützung in Eiffel

Die Programmiersprache Eiffel unterstützt Schleifeninvarianten nativ. Die Invarianten werden von der Sprache zur Laufzeit überwacht.

Im angegebenen Beispiel wird x zunächst auf 0 gesetzt. Die Schleifeninvariante lautet x <= 10. Die Schleife wird ausgeführt, solange die Abbruchbedingung x >= 10 noch nicht erfüllt ist, und erhöht x in jedem Durchlauf um 1. Sobald x den Wert 10 erreicht, wird die Schleife verlassen.

Die Invariante x <= 10 ist sowohl vor der Ausführung der Schleife als auch nach jeder Ausführung erfüllt. Das Beispiel hat daher die Form:

from x := 0 invariant x <= 10 until x >= 10 loop x := x + 1 end