DONE!

We have demonstrated systematically that

    { PRE }  program  { POST }

so 'program' is correct with respect to the specs 'PRE' and 'POST'

Note: There is no condition y > 0 in PRE... this means the program may not terminate.

This problem would not be discovered until we tried to do a termination proof.