Schleifeninvariante & While-Regel

Für Schleifen (while b do S od) gilt die Regel:

\frac{{P \land b} S {P}}{{P} w h i l e b d o S o d {P \land \neg b}}

Hierbei ist $P$ die Schleifeninvariante ( $I$ ). Sie muss vor der Schleife gelten, durch den Rumpf erhalten bleiben (wenn $b$ wahr ist) und nach der Schleife (wenn $b$ falsch ist) die gewünschte Nachbedingung implizieren.