Regel: Schleifen

       { 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;
}



Johannes Waldmann 2006-06-26