Proof Example: Exponentiation

Consider this program ( it computes x raised to power n ) :

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

      k, y, z := n, 1, x

      while k != 0 do

        if odd(k) 

          then k, y := k-1, y * z

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

        endif

      endwhile

   { POST: y = x^n }