Schleifeninvariante


Mit einer Schleifeninvariante können Vorgänge innerhalb einer Schleife besser erfasst und die formale Korrektheit eines Programmes bewiesen werden. So umfasst eine Schleifeninvariante Eigenschaften einer Schleife, die zu einem bestimmten Punkt bei jedem Durchlauf der Schleife gültig sind. Sie ist also eine Zusicherung, die unmittelbar vor Eintritt des Schleifendurchlaufs und nach jedem Schleifendurchlauf gilt. Dabei ist stets möglich eine Schleifeninvariante zu finden.

Es gibt meist nicht nur „die eine“ Schleifeninvariante in einem Programm. Und dennoch ist es nicht trivial eine Schleifeninvariante zu finden. So gibt es keinen Algorithmus um eine Schleifeninvariante automatisch zu bestimmen.

Um die Korrektheit einer Schleifeninvariante zu verifizieren, prüft man erst einmal ob sie bei der Initialisierung gilt und anschließend ob sie auch beim Übergang von einem Durchgang zum nächsten Durchgang erhalten bleibt. Für letzteres greift man beispielsweise auf den Beweis durch vollständige Induktion zurück.


Zitat:



Edsger Wybe Dijkstra:

"Als es noch keine Computer gab, gab es auch das Programmieren als Problem nicht. Als es dann ein paar leistungsschwache Computer gab, wurde das Programmieren zu einem kleinen Problem und nun, wo wir leistungsstarke Computer haben, ist auch das Programmieren zu einem riesigen Problem angewachsen. In diesem Sinne hat die elektronische Industrie kein einziges Problem gelöst, sondern nur neue geschaffen." - The Humble Programmer, ACM Turing Lecture 1972