program verification

Consider the following pseudo code, where x and y are positive integers. begin q := 0 r := x while r ≥ y do begin r := r - y q := q + 1 end end The post condition that needs to be...

An unrestricted use of the "goto" statement is harmful because