PROGRAM VERIFICATION

Handout #5


What does the following program do?
 

input(x,y)
z := 1
while y /= 0 do
    if odd(y)
        then (y,z) := (y-1,x*z)
        else (x,y) := (x*x,y/2)
output(z)