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 endendThe 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}