Putting in the prev y-m:

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