Schleifen-Invarianten

$$Id: invariant.tex,v 1.2 2003/11/20 14:09:12 joe Exp $$

static int power (int b, int e) {
   int p = 1; int q = b;
   while (e > 0) { 
      if (1 == e % 2) { p = p * q; }
      q = q * q; e = e / 2;
   }
   return p;
}

Der Ausdruck $A = p \cdot q^e$ ist invariant:

seine Werte vor und nach Ausführen eines Schleifenkörpers stimmen überein.