Regel: Schleifen

       { 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