Axiom für Schleifen

wenn  { I and B } A { I },
dann  { I } while (B) do A { I and not B }

Beispiel:

Eingabe int p, q; 
// p = P und q = Q
int c = 0;
// inv: p * q + c = P * Q 
while (q > 0) { 
   ???
}
// c = P * Q

Moral: erst Schleifeninvariante (Spezifikation), dann Implementierung.