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 }