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

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 Correct Answer {x = qy + r ∧ r < y}

code is doing division by subtraction. Y is being subtracted repeatedly from r until it is less than y.

∴ At the end:

[ alt="zza18" src="//storage.googleapis.com/tb-img/production/17/03/zza18.JPG">