Schleifeninvariante
Als Schleifeninvariante werden Eigenschaften einer Schleife in einem Computerprogramm bezeichnet, die zu einem bestimmten Punkt bei jedem Durchlauf gültig sind, unabhängig von der Zahl ihrer derzeitigen Durchläufe.
Typischerweise enthalten Schleifeninvarianten Wertebereiche von Variablen und Beziehungen der Variablen untereinander.
Schleifeninvarianten werden benötigt zur Verifizierung von Programmen und helfen zudem die Vorgänge innerhalb einer Schleife besser zu erfassen und die Korrektheit eines Algorithmus zu beweisen.
Beim Korrektheitsbeweis für einen Algorithmus mittels einer Schleifeninvariante ist folgendes zu zeigen: Initialisierung, Aufrechterhaltung, Beendigung
Zu allen drei Zeitpunkten muss die Schleifeninvariante korrekt sein, dh. Variablen müssen innerhalb definierten Bereichen liegen, Input-Arrays dürfen bei einem Sortierverfahren nicht wertmäßig verändert werden, sondern nur die Reihenfolge darf angepasst werden. Diese Punkte müssen wie gesagt während allen drei Phasen gewährt sein.
Beispiel Multiplikation
x:= a; y:= b; p := 0; while x > 0 do begin p:= p + y; x:= x-1; end;
Dieser Algorithmus multipliziert die Zahl "a" mit der Zahl "b" durch Addition.
Die Schleifeninvariante für diesen Algorithmus lautet: x*y+p = a*b.