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 satisfied after the program terminates is

• A. {r = qx + y ∧ r < y}
• B. {x = qy + r ∧ r < y}
• C. {y = qx + r ∧ 0 < r < y}
• D. { q + 1 < r–y ∧ y > 0}