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