Oct 30 - Week 8

Since I missed this Monday's lecture, I'd decide to go to the evening instead. Surprisingly, I found the evening lecture is much better than the morning sections. Perhaps it's because there are fewer people prefer to listen a lecture in the evening.

We went through the pow_revisited example, which contains one simply while loop. It was quite obvious and meant to show us the structure of proving a loop is correct. The "trickier termination" is indeed tricker. A girl came up with the question with what if value a become negative? I was wondering the same thing at that time either. Well fortunately a won't be decremented as long as b is not zero, and in that case this statement is assumed. This would be the trickiest part, as only every time b becomes zero, a will decrement by 1, and b's value will be back to 6 again. It's not that obvious to figure out what the loop is behaving at the first place. And this is not the worst, the last example is a selection sort function, which contains two for loops. The algorithm is not hard, but you will likely yo lose the track of in dices as you are writing the proof. As Professor Danny said, never use any letter that is a index in the program in your proof, since that will really drive us into trouble.

Besides, we also need to check if the loop is ever going to end. At this point I like for loop more, as most of the time it has a finite set of content to iterate. For while loop I have to check the statement which it moves the iteration forward. Luckily if there is more than one condition along with the while loop, it will generate cases.

Overall, I do believe I kind of get what I am supposed to do when I were to write a proof about a loop --- that is, to find out the pre and post condition (wonder if there is any chance that these two conditions are given in the questions?), find out an expression of what the loop does (not sure what officially that calls) and try to make sure the loop ends.

Oct 28 - Week 8

Last week we did a proof about the binary search. I begin to doubt is it always the case that we use strong induction to prove the program correctness? At least for now I assume so. The proof structure is not quite complexed. Just as normal strong induction, we will assume P(1) up to P(n-1). As the programming code come into play now, we have to analyze what does these code do at the same time. Binary search has got a basic case, which is the input first index and last index is the same. It means we go through the entire list, so the if the index position indeed contains the element we want, then we are done. Otherwise we can not find anything, since we assumed the entire list has been gone through. This satisfies both precondition as well as postcondition. After finished the base case, we will play with the rest of the program for a well. The key part is how the program divide the list into two parts. That generate the proof into two separate branches. First is the list from the first to the m index, the other one runs from m+1 to the last. By comparing the element to the value of m, it will make the list smaller and smaller. We can not forget to check whether the precondition still holds at the same time.
The greatest common divisor example seems ambiguous to me. I sort of understanding how the proof is made, but have some problems understanding how does the program works.

I missed Monday's lecture, and did not have a chance to hand in the problem set 4 which was printed two days ago. I believe I will go to Thursday evening's lecture.

Oct 20 - Week 7

Professor Danny was missing today, but that doesn't mean we didn't have a passionate class. Instructor Nick starts the class with a statement "No programs will never crush.". Quite interesting, eh? He then lead us go through the Binary Search algorithm. By that he introduced us "Precondition" and "Postcondition". The postcondition is guaranteed to happen provided the correct precondition is given.

Sept 29th - Week 3

On today's lecture we begin to touch some aspects of the recursion and its proof.
We started by proving a recursive f(n) which f(n) = 0 if n =0, otherwise f(n) = f(n-1) + 3n^2.
Then we get into the Fibonacci sequences by a rabbit example. We tried a few base cases and figured out some patterns between the summation of the entire sequences and F(n).

Sept 24th - Week 2

On Monday we have discovered "Principal of well ordering".

Today we have gone back to some simple induction proofs.

Sept 15 - Week 2

In today's lecture we escaped from simple induction proof and instead we will have strong or complete induction. The professor uses two examples to show how complete induction applies.

Instead of simple induction which need one or a few base cases and then all other possible cased can be proved by the base case, the strong induction needs all the n-1 cases to be true in order to prove the "n"th to be true.

Week 1

Starting Week.
First few lectures are acceptable but still takes a while to catch up with everything.