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.