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.