Schleifeninvariante

In der Informatik ist eine Schleifeninvariante eine Sonderform der Invariante, die am Anfang und Ende eines jeden Schleifendurchlaufs und vor und nach der Ausführung der Schleife in einem Algorithmus gültig ist. Sie ist damit unabhängig von der Zahl ihrer derzeitigen Durchläufe. Eine Schleifeninvariante wird zur formalen Verifizierung von Algorithmen benötigt und hilft zudem, die Vorgänge innerhalb einer Schleife besser zu erfassen. Typischerweise beschreiben Schleifeninvarianten Wertebereiche von Variablen und Beziehungen der Variablen untereinander. Da es sich bei der Schleifeninvariante um einen logischen Ausdruck handelt, kann sie entweder wahr oder falsch sein.

Zu jeder Schleife lässt sich eine Invariante finden, die vor der Schleife und nach jeder Prüfung der Schleifenbedingung gilt, z. B. eine Tautologie wie „wahr = wahr“. Es lässt sich also immer eine Invariante bestimmen, diese ist aber nicht immer dafür geeignet, einen formalen Korrektheitsbeweis durchzuführen.

Korrektheitsbeweis

Entsprechend dem Hoare-Kalkül ist beim Korrektheitsbeweis einer Schleife mittels einer Schleifeninvariante zu zeigen, dass die Schleifeninvariante direkt vor der Ausführung der Schleife und nach jeder Prüfung der Schleifenbedingung gültig ist. Nach der Prüfung der Schleifenbedingung kann die Schleife entweder betreten werden (Schleifenbedingung erfüllt) oder verlassen werden (Schleifenbedingung nicht erfüllt). Deshalb muss die Invariante sowohl direkt am Anfang jedes Schleifendurchlaufs gelten als auch direkt nach der Schleife (siehe Beispiel).

Partielle Korrektheit

Für die partielle Korrektheitsüberprüfung prüft man zuerst, ob die Invariante beim ersten kritischen Zeitpunkt gilt, also direkt vor der Schleife. Danach wird geprüft, ob sie beim Übergang von einem Durchgang zum nächsten erhalten bleibt. Dieses Vorgehen entspricht der vollständigen Induktion der Mathematik. Außerdem muss die Invariante auch direkt nach der Schleife gelten. Zu allen drei Zeitpunkten muss die Schleifeninvariante korrekt sein, d. h. Variablen müssen z. B. innerhalb definierter Bereiche liegen oder gewisse Beziehungen zueinander haben.

Nach dem Verlassen einer Schleife, bei der die Invariante nicht verletzt wird, gelten die abweisende Schleifenbedingung (sonst wäre die Schleife nicht verlassen worden) und die Schleifeninvariante. Wenn sich aus diesen beiden logischen Ausdrücken das gewünschte Ergebnis der Schleife durch und-Verknüpfung ergibt, dann ist die partielle Korrektheit der Schleife bewiesen. Partielle Korrektheit bedeutet, dass immer, wenn die Schleife terminiert (verlassen wird), das korrekte Ergebnis vorliegt. Damit ist jedoch nicht bewiesen, dass die Schleife immer terminiert (totale Korrektheit).

Totale Korrektheit

Um die totale Korrektheit einer Schleife zu beweisen, muss zunächst die partielle Korrektheit bewiesen werden. Anschließend wird geprüft, ob die Schleife immer terminiert. Dazu muss zunächst ermittelt werden, wann die Schleife verlassen werden kann. Wenn sie verlassen werden kann, muss nachgewiesen werden, dass sie das in jedem Fall tut, z. B. die Zählervariable einer For-Schleife erhöht sich bei jedem Durchlauf bis zu einer Obergrenze und wird innerhalb der Schleife nicht verändert.

Wenn so nachgewiesen ist, dass die Schleife immer terminiert und dass anschließend immer das gewünschte Ergebnis vorliegt, ist die totale Korrektheit der Schleife bewiesen.

Es ist bewiesen, dass es keinen Algorithmus gibt, der automatisiert für alle Schleifen eine Schleifeninvariante findet, die für einen Korrektheitsbeweis verwendet werden kann.

Beispiel

Der folgende Algorithmus multipliziert die beiden Variablen a und b miteinander:

 multiply(a, b) {
   x := a;
   y := b;
   p := 0;
   // die Invariante muss vor der Schleife gelten
   while x > 0 do {
      // die Invariante muss am Anfang jedes Durchlaufs gelten
      p := p + y;
      // innerhalb der Schleife muss die Invariante nicht gelten;
      // (x * y) + p = a * b ist an dieser Stelle nicht erfüllt
      x := x - 1;
      // die Invariante muss auch am Ende jedes Durchlaufs gelten
   }
   // die Invariante muss auch direkt nach der Schleife gelten
   return p
 }

Eine Schleifeninvariante für diesen Algorithmus lautet:

$(x\cdot y)+p=a\cdot b$

Native Unterstützung durch Programmiersprachen

Eiffel

Die Programmiersprache Eiffel bietet nativ Schleifeninvarianten an. Die Invarianten werden von der Programmiersprache zur Laufzeit überwacht.

Im folgenden Beispiel wird die Invariante x <= 10 für die Schleife definiert. Die Schleife läuft so lange, bis x den Wert 10 erreicht hat. Dann wird die Schleife verlassen. Die Invariante ist im Beispiel sowohl vor der Ausführung der Schleife als auch nach jeder Ausführung der Schleife erfüllt.

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

Siehe auch

• wp-Kalkül