PROGRAM VERIFICATION

Handout #2


The following program is intended to restructure a binary tree so that it becomes its mirror image.
 

Reflect(t):
init-stack(s)
push(t,s)
while not empty?(s) do
    r := top(s)
    pop(s)
    if not leaf?(r) then
        temp := right(r)
        right(r) := left(r)
        left(r) := temp
        push(left(r),s)
        push(right(r),s)
return(t)