# 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 $k \in \mathbb{N}$, if $k$ is odd then on the $k+1$ -st trip around the loop at the top of the loop $a=-2(k+1),\ b=k(-1)^{k+1}=k$.

Now at the end of the loop:

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

and:

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

(note in the last line the value of $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 $k$ is even, at the top of the look after the k-th itteration: $a=2k,\ b=k(-1)^{k+1}=-k$

and at the end of the loop:

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

and:

$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