The loop invariant

Computer Science Level 2

p=1
i=0
while p<n:
    p=2*p
    i+=1

Consider the above fragment of code, with $n$ , $p$ and $i$ as integer variables. What is the loop invariant of the code?

Definition : A loop invariant is a condition that is necessarily true immediately before and immediately after each iteration of a loop

p=(i+1)^{2}

p=2^{i}

p=2^{i+1}

p=(i+1)2^{i}

p=i+1

2 solutions

Agnishom Chattopadhyay
Jul 2, 2016

[ Initiation ] Before the loop, $i = 0$ and $p = 1$ . Hence, $p = 2^i$
[ Iteration ] Assume that before an iteration, we have $i = i'$ and $p = 2^{i'}$ . Line 4 changes $p \leftarrow 2 p = 2 \cdot 2^{i'} = 2^{i' + 1}$ and line 5 changes $i \leftarrow i'+1$

Hence, by induction, after any iteration $p = 2^i$ holds.

Sam Bealing
Jun 28, 2016

The situation after $k \: loops$ is that $p=2^k$ and $i=k$ it therefore follows the loop invarient is $\boxed{\boxed{p=2^i}}$

Not quite. You have to explain why the step of the loop doesn't change the fact that $p = 2^i$ .