GATE CS 2015 Set 1 Q.43 (CS Q.33): Data Types, Operators and Control Flow

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:

$\{r = qx + y \land r < y\}$

$\{x = qy + r \land r < y\}$

$\{y = qx + r \land 0 < r < y\}$

$\{q + 1 < r - y \land y > 0\}$

Official answer and solution

Solution

Determine the loop invariant and termination condition of the standard integer division algorithm.

The algorithm implements integer division of positive integer $x$ by positive integer $y$ using repeated subtraction:

Initially: $q = 0, r = x$ .
At initialization: $x = 0 \cdot y + x = q \cdot y + r$ .
Loop body: at each step, $r$ is decremented by $y$ and $q$ is incremented by $1$ : $(q + 1)y + (r - y) = qy + y + r - y = qy + r = x.$ Thus, the loop invariant $x = qy + r$ holds throughout.
Termination: the while loop while r >= y terminates when $r \ge y$ becomes false, i.e., $r < y$ .

Combining the invariant and termination condition:

\{x = qy + r \land r < y\}.

This matches option B.

Final answer

Common trap

Switching $x$ and $y$ in the division formula or postcondition relation.

The answer is the one in the official GATE answer key. The solution is this site's own explanation.

GATE questions are the work of the organising institutes. This site is independent and is not affiliated with them.