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.