Schleifeninvariante

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

In der Informatik ist eine Schleifeninvariante eine Sonderform der Invariante, die vor, während und nach der Ausführung einer Schleife in einem Algorithmus gültig ist[1]. 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[Bearbeiten]

Entsprechend des Hoare-Kalküls 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 komplett 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[Bearbeiten]

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[2]. 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 etwa innerhalb definierter Bereiche liegen.

Nach dem Verlassen einer Schleife, bei der die Invariante nicht verletzt wird, gilt 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), liegt das korrekte Ergebnis vor. Damit ist jedoch nicht bewiesen, dass die Schleife immer terminiert (totale Korrektheit).

Totale Korrektheit[Bearbeiten]

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 nachgeiwesen 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[Bearbeiten]

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

  1.  multiply(a, b) {
    
  2.    x := a; 
    
  3.    y := b;  
    
  4.    p := 0;
    
  5.    // die Invariante muss vor der Schleife gelten
    
  6.    while x > 0 do {
    
  7.       // die Invariante muss am Anfang jedes Durlaufs gelten
    
  8.       p := p + y;
    
  9.       // innerhalb der Schleife muss die Invariante nicht gelten,
    
  10.       // (x * y) + p = a * b ist dieser Stelle nicht erfüllt
    
  11.       x := x - 1;
    
  12.    }
    
  13.    // die Invariante muss auch direkt nach der Schleife gelten
    
  14.    return p
    
  15.  }
    

Eine Schleifeninvariante für diesen Algorithmus lautet:

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

Native Unterstützung durch Programmiersprachen[Bearbeiten]

Eiffel[Bearbeiten]

Die Programmiersprache Eiffel bietet nativ Schleifeninvarianten an[3]. 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 durch, 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[Bearbeiten]

Einzelnachweise[Bearbeiten]

  1.  Martin Glinz, Harald Gall: Systematisches Programmieren: Lesbare und änderbare Programme schreiben. In: Software Engineering. 2005, S. 39-40 ([1], abgerufen am 11. April 2014).
  2.  Edsger Wybe Dijkstra: Some beautiful arguments using mathematical induction. In: Acta Informatica. Nr. 13, 1980, S. 1-8.
  3. Meyer, Bertrand, Eiffel: The Language, Prentice Hall, 1991, S. 129–131.