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 }Prove that the program is correct with respect to the given PRE and POST specifications...