GATE CS 2015 Set 1 Q33 — Programming in C

The given pseudocode implements the standard integer division algorithm to divide a positive integer $x$ by another positive integer $y$, where $q$ represents the quotient and $r$ represents the remainder.

1. Identifying the Loop Invariant

Before entering the loop, we initialize:

• $q = 0$
• $r = x$

At this initial state, the relation $x = qy + r$ holds because:

$$qy + r = (0 imes y) + x = x$$

In each iteration of the loop, the variables are updated as follows:

• $r_{\text{new}} = r - y$
• $q_{\text{new}} = q + 1$

Let's check if the relation still holds after these updates:

$$q_{\text{new}}y + r_{\text{new}} = (q + 1)y + (r - y) = qy + y + r - y = qy + r = x$$

Since the relation remains unchanged, $x = qy + r$ is a loop invariant.

2. Termination Condition

The loop runs as long as $r \ge y$. Therefore, when the loop terminates, the loop condition must become false:

$$\neg(r \ge y) \implies r < y$$

3. Post-Condition

Upon termination, both the loop invariant and the termination condition must hold simultaneously. Thus, the post-condition is:

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

This matches Option B.