{ V und B } P { V } ------------------------------------ { V } while B do P { V und nicht B }
V
heißt Invariante der Schleife
Beispiel (schnelles Potenzieren)
int power (int b, int e) { int p = 1; while (e > 0) { // inv: b^e * p if (odd (e)) { p = p * b; } b = b * b; e = e / 2; // abgerundet } return p; }Beweise
power (b,e) = b^e