Program to compute x**y:

Where x, y, and z are of type Z (int):

{y >= 0}
z := 1;
{y >= 0 & z = 1}
m := 0;
{y >= 0 & 0 <= m <= y & z = x**m}
while m < y do
    {y >= 0 & 0 <= m <= y & z = x**m & m < y}
    {y >= 0 & 0 <= m < y & z = x**m}
    z := z * x;
    {y >= 0 & 0 <= m < y & z = x**m * x}
    m := m + 1;
    {y >= 0 & 0 <= m <= y & z = x**m}
end while
{y >= 0 & 0 <= m <= y & z = x**m & m >= y}
{m = y & z = x**m}
{z = x**y}