Tutorial 3

This tutoria is for the concept of Q2 from a3
I don't have an example on mind right now so I'm just going to talk about the general procedure instead of doing example for this tutorial

For Q that given you the precondtion and ask you to come up with a loop invariant and prove for termination  First there is 2 parts the question: It is actually asking you to prove 1)partial correctness and 2) termination. Notice I said and, not or, so you have to prove BOTH of them in order to prove it terminates.

For partial correctness part. First thing you want to come up is come up a loop invariant. Loop invariant is a condition statement which while the loop is still running, the statement condition is always true. If some sort of  part your loop invariant is false(excluding termination), then you may want to think again about your loop invariant. Finding loop invariant is always  the most tricky part of the question. Sometime it's so oblivious you don't have to trace through to see it, while other are the opposite. I went to the prof during office and ask if there's any general formula to find a loop invariant, and the answer is no. So be patient while finding it.

Once you find the loop invariant, you   may want to prove the loop condition before the first loop being executed. This ensures that before the loop execute, your loop condition holds, or else your loop invariant is wrong.

Once you did that, now you may want to define P(i), where i is the time of iteration. And you may want to make the P(i) be the loop invariant you come up with plus pre condition. Once you set up though, you may want to set up a simple induction.

So for base case, it's always easier to make i = 0, as it is just the loop before it got executed the first time.
For P(i +1), you want want to get a IH that is similar to this format:
Assume i is a arb Natural Number and P(i) is true
Then go ahead and solve the P(i+1)
After you finish the simple induction, you have completed the partial correctness part, there's still the termination part...

To prove termination, Since we are given the loop will run and loop invariant is true, now what we want to do it that reverse the condition of  the while loop (or any main loop that the program runs based on), ex (while x <y), you may want to make it (while x>=y). In here, how to do it is up to you, either induction or not, as long as you can show the loop will eventually terminates, that's what matters.

I hope this tutorial clears something out. Good luck on your a3!