Scribd
Upload
23 views2 pages

Loop Invariant

Uploaded by

bhattifarhan182
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
23 views2 pages

Loop Invariant

Uploaded by

bhattifarhan182
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
You are on page 1/ 2

Algorithms [Compiled on February 18, 2011] Spring 2011

Note on Chapter 2 of [Manber]:


Proving a Loop Invariant

Below is the program given in Chapter 2 (Page 27) of Manber’s book that converts a decimal
number into a binary one:

Algorithm Convert to Binary (n);


begin
t := n;
k := 0;
while t > 0 do
k := k + 1;
b[k] := t mod 2;
t := t div 2;
end

Let Inv(n, t, k, b) denote the following assertion:

n = t × 2k + m and t ≥ 0,
where(m is the binary number represented by b, i.e.,
0 if k = 0
m= k−1 k−2 0
b[k] × 2 + b[k − 1] × 2 + · · · + b[1] × 2 if k ≥ 1

Claim: Inv(n, t, k, b) is a loop invariant of the while loop, assuming that the decimal number
passed via variable n is non-negative. (The invariant is sufficient to deduce that, when the
program terminates, b stores the binary representation of n.)
Proof: The proof is by induction on the number of times the loop body is executed. More
specifically, we show that (1) the assertion is true when the flow of control reaches the loop for
the first time and (2) given that the assertion is true and the loop condition holds, the assertion
will remain true after the next iteration (i.e., after the loop body is executed once more).
(1) When the flow of control reaches the loop for the first time, t = n (≥ 0) and k = 0. With m
denoting the binary number represented by b, t × 2k + m = n × 20 + 0 = n and t ≥ 0. Therefore,
the assertion Inv(n, t, k, b) holds.
(2) Assume that Inv(n, t, k, b) is true at the start of the next iteration and the loop condition
(t > 0) holds. Let n0 , t0 , k 0 , and b0 denote respectively the values of n, t, k, and b after the next
iteration. We need to show that Inv(n0 , t0 , k 0 , b0 ) also holds.

1
From the loop body, we deduce the following relationship:

k0 = k + 1
b0 [k 0 ] = t mod 2
b0 [i] = b[i] for all i 6= k 0
t0 = t div 2
n0 = n (the value of n never changes)

There are two cases to consider: when t is odd and when t is even. We prove the first case;
the second case can be proven similarly. If t is odd, t mod 2 contributes 1 to b0 [k 0 ]. The
0 0
binary number m0 represented by b0 equals b0 [k 0 ] × 2k −1 + b0 [k 0 − 1] × 2k −2 + · · · + b0 [1] × 20 =
0 0
2k −1 + b[k] × 2k−1 + b[k − 1] × 2k−2 + · · · + b[1] × 20 = 2k + m. We then have t0 × 2k + m0 =
t−1
2 × 2k+1 + 2k + m = (t − 1) × 2k + 2k + m = t × 2k + m = n = n0 . In addition, since t > 0
(given that the loop condition holds), t0 = t div 2 ≥ 0. Therefore, Inv(n0 , t0 , k 0 , b0 ) holds after
the next iteration in the case of odd t.

You might also like