Exponentiation Proof

{ PRE: n >= 0 and x != 0 }

   k, y, z := n, 1, x
   { INV: k>=0 and x^n=y*z^k and x!=0 and z!=0 }
   while k != 0 do

     if odd(k) 
       { P2: (k-1)>=0 and x^n=(y*z)*z^(k-1) and x!=0 and z!=0 }
       then k, y := k-1, y * z

       else k, z := k/2, z * z

     endif
     { INV: k>=0 and x^n=y*z^k and x!=0 and z!=0 }
   endwhile

{ POST: y = x^n }