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

Thanks in advance.

Printable View

- Feb 24th 2008, 10:53 AMshawnProving 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.

Thanks in advance. - Feb 24th 2008, 11:38 AMCaptainBlack
- Feb 24th 2008, 11:46 AMshawn
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, 06:21 PMshawn
Anyone? pleease!

- Feb 25th 2008, 09:38 PMCaptainBlack
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 , if is odd then on the -st trip around the loop at the top of the loop .

Now at the end of the loop:

and:

(note in the last line the value of 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 is even, at the top of the look after the k-th itteration:

and at the end of the loop:

and:

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

RonL