# Proving correctness of a loop using Induction

• Feb 24th 2008, 09:53 AM
shawn
Proving correctness of a loop using Induction
I was hoping someone could help me solve this question, or even just give me a good idea on how to start it.

• Feb 24th 2008, 10:38 AM
CaptainBlack
Quote:

Originally Posted by shawn
I was hoping someone could help me solve this question, or even just give me a good idea on how to start it.

For part (a) ask what value i has when the loop is exited, then compare this with the loop invariant.

RonL
• Feb 24th 2008, 10:46 AM
shawn
Quote:

Originally Posted by CaptainBlack
For part (a) ask what value i has when the loop is exited, then compare this with the loop invariant.

RonL

I think I have to prove that the invariant is true for I(0) which is the basis which is easy, and then assume the ith works, and prove i+1 works, and then prove that it terminates correctly and then I'll have the full proof.

It's easy to just figure out the values like you suggest and say yes, 1=1 so it is correct, but that's not a formal enough proof, it just tells us that it should be correct.
• Feb 25th 2008, 05:21 PM
shawn
Anyone? pleease!
• Feb 25th 2008, 08:38 PM
CaptainBlack
Quote:

Originally Posted by shawn
I think I have to prove that the invariant is true for I(0) which is the basis which is easy, and then assume the ith works, and prove i+1 works, and then prove that it terminates correctly and then I'll have the full proof.

It's easy to just figure out the values like you suggest and say yes, 1=1 so it is correct, but that's not a formal enough proof, it just tells us that it should be correct.

Well the question as asked does not ask for a proof of the invariant, but

You can show the base cae is true, now suppose the invariant holds for some $\displaystyle k \in \mathbb{N}$, if $\displaystyle k$ is odd then on the $\displaystyle k+1$ -st trip around the loop at the top of the loop $\displaystyle a=-2(k+1),\ b=k(-1)^{k+1}=k$.

Now at the end of the loop:

$\displaystyle b=-2(k+1)+k+1 = -k-1=-1(k+1)=(k+1)(-1)^{k+1}$

and:

$\displaystyle a=-2(k+1)+4(k+1)=2(k+1)$

(note in the last line the value of $\displaystyle b$ used is that produced by the previous line not what it was at the top of the loop)

So the invariant holds in this case.

Now if $\displaystyle k$ is even, at the top of the look after the k-th itteration: $\displaystyle a=2k,\ b=k(-1)^{k+1}=-k$

and at the end of the loop:

$\displaystyle b=2k-k+1=k+1=(k+1)(-1)^{k+2}$

and:

$\displaystyle a= 2k-4(k+1)=-2k-4=-2[(k+1)+1]$

so the invariant holds in this case also, and so the given loop invariant is indeed a loop invariant for this loop.

RonL