Schleifeninvariante
Bedeutung
Sei W = while(b){S} eine Schleife mit seiteneffektfreier Bedingung b.
Eine Schleifeninvariante INV zur Schleife W ist ein boolescher
Ausdruck/eine logische Formel mit der Eigenschaft:
{ b && INV } S { INV }
Bemerkungen
Die zentrale Schwierigkeit bei der Verifikation von nicht-rekursiven prozeduralen Programmen ist das Entwickeln geeigneter Schleifeninvarianten.
Schleifeninvarianten sind auch ein hervorragendes Dokumentationsmittel, da sie die algorithmische Idee ausdrückt, die der Schleife zugrunde liegt.