Schleifeninvariante

Als Schleifeninvariante werden Eigenschaften einer Schleife in einem Algorithmus bezeichnet, die zu einem bestimmten Punkt bei jedem Schleifendurchlauf gültig sind, unabhängig von der Zahl ihrer derzeitigen Durchläufe. Sie werden zur Verifizierung von Algorithmen benötigt und helfen zudem, die Vorgänge innerhalb einer Schleife besser zu erfassen. Typischerweise beschreiben Schleifeninvarianten Wertebereiche von Variablen und Beziehungen der Variablen untereinander.

Zu jeder Schleife lässt sich eine Aussage finden, die vor und nach der Schleife gilt, z. B. eine Tautologie wie „wahr = wahr“. Es ist also stets möglich, eine Invariante anzugeben.

Korrektheitsbeweis

Beim Korrektheitsbeweis für einen Algorithmus mittels einer Schleifeninvariante ist zu zeigen, dass die Schleifeninvariante bei Initialisierung, Aufrechterhaltung und Beendigung der Schleife eingehalten wird. Die Korrektheitsüberprüfung lässt sich zweiteilen. Hierzu prüft man zuerst, ob sie beim ersten kritischen Zeitpunkt gilt, ob sie also initialisiert ist. Schließlich wird geprüft, ob sie beim Übergang von einem Durchgang zum nächsten erhalten bleibt. Dieses Vorgehen entspricht der vollständigen Induktion der Mathematik. Zu allen drei Zeitpunkten muss die Schleifeninvariante korrekt sein, d. h. Variablen müssen etwa innerhalb definierter Bereiche liegen. Außerdem dürfen z.B. Input-Arrays bei einem Sortierverfahren nicht wertmäßig verändert werden, sondern nur die Reihenfolge darf angepasst werden.

Es ist bewiesen, dass es keinen Algorithmus gibt, der eine Schleifeninvariante automatisch bestimmt.

Beispiel

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

x := a; 
y := b;  
p := 0;
while x > 0 do
begin
  p := p + y;
  x := x - 1;
end;

Eine Schleifeninvariante für diesen Algorithmus lautet:

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

Siehe auch

• Hoare-Kalkül
• Invariante (Informatik)