Gegeben sei das Beispielprogramm:
{x = n}
y := 1; while (x != 1) do (y := x * y; x := x - 1) od
{y = n! and n > 0}
Wenn jetzt x = n vor der Ausführung gilt, und dann y = n! nach der Ausführung (sofern die Ausführung terminiert) gilt, spricht man von partieller Korrektheit.
Wenn x = n vor der Ausführung gilt, dann terminiert das Programm und dann hat y den Wert n!, dann spricht man von totaler Korrektheit.
Zusammengefasst:
Wenn die Schleifentermination nicht garantiert werden kann, dann wird die axiomatische
Beschreibung der Schleife partielle Korrektheit genannt.
Schleifentermination, die bewiesen werden kann, nennt man totale Korrektheit.