engl.: loop invariant

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 }

• 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.