edited by
15,385 views
54 votes
54 votes

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

  1. $\{ r = qx + y \wedge r < y\}$
  2. $\{ x = qy  + r \wedge r < y\}$
  3. $\{ y = qx + r \wedge 0 < r < y\}$
  4. $\{ q + 1 < r - y \wedge y > 0\}$
edited by

7 Answers

Best answer
70 votes
70 votes

Correct Option: B

The loop terminates when $r < y$. So, $r < y$ is one post condition. 

In each iteration $q$ is incremented by $1$ and $y$ is subtracted from $r$. Initial value of $r$ is $x$. So, loop iterates $x/y$ times and $q$ will be equal to $x/y$ and $r = x\%y \Rightarrow x = qy + r;$ 

edited by
16 votes
16 votes

Just take an example and try to solve it by using options:

suppose, x=10 and y=5

begin 
    q := 0  // q = 0
    r := x  // r = x i.e. r = 5 as value of taken as 10
   while r ≥ y do  // 10 ≥ 5 ; TRUE     (first iteration)
      begin 
      r := r - y  // r = 10 - 5 = 5
      q := q + 1  // q= 0 + 1 = 1
    end 
   while r ≥ y do // 5 ≥ 5 ; TRUE        (second iteration)
      begin 
      r := r - y // r = 5 - 5 = 0 
      q := q + 1 // q= 1 + 1 = 2
    end 
  while r ≥ y do // 0 ≥ 5 ; FALSE         (third iteration)
end

at the end of while loop

we get value of r = 0 and q = 2

x= 10 and y = 5

Now one by one put these values in given option 

and thus, option B satisfied i.e. 

{x=qy+r∧r<y}   // x = 2*5 + 0 = 10 and 0 < 5

14 votes
14 votes
post condition :-

the loop terminates when ( r<y ) so one condition { r<y }

( q=q+1 ) q is increasing every time by 1 so q is simply counting loop count.

so r after execution

r = r - q y

(r=x) so

r = x - q y

x = r + q y

so option B

x = r + qy ^ r < y
Answer:

Related questions

24 votes
24 votes
3 answers
3
Kathleen asked Sep 12, 2014
4,357 views
Consider the following PASCAL program segment:if i mod 2 = 0 then while i >= 0 do begin i := i div 2; if i mod 2 < 0 then i := i - 1; else i := i – 2; end;An appropria...