Tutorial 2 repost

Sorry I deleted my tutorial 2 by mistake, so I have to type all those stuff again... Since my original post is almost 2 pages long, I'm going to short form this tutorial, since I got 2 more assignments coming up due last that 2 and 4 days and I'll busying finishing those, please understand...
This tutorial talks about the concept behind Q2 of our a3

If you are given a loop, and pre condition, prove proof it will terminate

First thing, This Q is actually 2 part Q: you have to prove partial correctness AND termination. Proof either one of those will not be enough.

For partial correctness, come up with a loop invariant, loop invariant is a condition statement that stays true throughout the whole loop as long as it is running. Then, assume the pre condition is true, proof that loop invariant is true before the first iterate occurs. After that, come up with a P(i) that is your loop invariant + pre condtion. Then proof P(i) by simple induction. first step proof P(i). When that's simple, that's exactly the proof for loop invariant is true before the first iterate occurs. Then we have to prove P(i+1). In order to do that, come up with a IH where assume i belongs arb Natural Number and P(i) holds, then proof the whole thing to get P(i+1), then P(i) => (P+1), which by simple induction, partial correctness is proved.

Now for Termination. We don't have to actually write induction all the time, All we have to do is assume the loop invariant is true, trace through the loop and show it eventually terminates. that's all.

Sorry for the simplified version, again sorry and please understand...
That's all, good luck on a3Q