Tutorial 4

This will be the last tutorial for a3, and is for Q4
Since the basic concept of this Q is similar to a2, this will be a short one, since I don't want to any waste too much time read similar concept

So in the Q, we are given pre condition and post condition, we are asked to prove that if the precondition is satisfie d, then your algorithm terminates and satisfie d the post-condition

What we want to do, similar to Q2, of course is to come up with a loop invariant! Question get so much easier with a loop invariant, whether you use it in your actual proof or not.

All you want to do it Assume the pre-condition is true, then prove that your loop invariant is true. Some approach maybe prove that invariant holds before the first loop is executed. I found that this is the easiest case to do it.

Then after proved that our loop invariant is true, now we assume the loop terminates and use the loop invariant to prove after it terminates, the post condition still holds. This is the different part from Q2, we can just assume the loop will terminate instead of proving it because we are given post condition, which post condition only stays true to those that are after the loop terminates. This implies the loop will eventually terminates, which is stupid to prove it terminates. If you still want to do it, be my guest, not like you are going to get extra marks but extra work, so why bother?

After you use loop invariant to prove postcondition, then you're all set, but what about the steps? Well, In order to prove something, aren't we always use induction? I'm going to use simple induction, where P(i) is the loop invariant + pre condition. The base case you may want to use something that terminate the loop instantly so that you can show the post condition show right away. for P(i+1), the IH should be i belong arb Natural Number and P(i) holds, and  it's is the same procedure: Assume the loop will terminate, then use your loop invariant to proof your post condition. After you proof  P(i) and P(i+1), then you proof the whole question by simple induction

I hope that help you with your a3, and good luck everyone!