EWD249 - 18

"x:= A; y:= B; z:= 1;
 while y ≠ 0 do
   begin if odd(y) do begin y:= y - 1; z:= z * x end;
         y:= y / 2; x:= x * x
   end"

finally

z = A^B   will hold.

The proof has to show that (in spite of "y:= y / 2") all variables keep integer values; the method shows the invariance of

x > 0 and y ≥ 0 and A^B = z * x^y   .