Correctness--the most tedious part

I have to say proving correctness is the most tedious part among this course. It involves lots of formats and conventions, and we have to remember and even recite those stuffs in order not to lose marks.

I have already read the textbook and made a summary about how to cope with questions concerning proving correctness.

There are two types of questions according to the textbook and the lecture notes: correctness on recursion and correctness on iteration.

For the first type of question(example: binary search), we need to state the precondition and postcondition at the beginning, and then i> prove partial correctness of BinSearch ii> prove termination of BinSearch.

For the second type of question(example: integer power of x), we also need to state the precondition and postcondition at the beginning, and then i> prove partial correctness of intPower ii> prove termination of intPower iii> derive the invariant in intPower.

I think knowing an outline of the whole solution can help us deal with those problems quicker and better.


But when I was trying to finish Assignment 3, I found my outline for solving the second type of problems did not work properly. So I had to derive a new guideline for solving the assignment problems.

When you get an algorithm and figure out what precondition and postcondition are, the next thing you must do is trying to figure out (largely by observing) the loop invariant after ith of the loop, and then using induction to prove it is correct.

After that, you must prove partial correctness, that is, assuming the program terminates, the final state (simply call it state after kth iteration) exactly meets the postcondition. In other words, It means if the program halts, the output is exactly what it is supposed to be.

Then you need to prove termination by proving the sequence of a certain variable (usually the variable determining the halt condition) is decreasing, then by WOP the whole program terminates.

Finally you can simply state that putting them together we get correctness (cheers!)

That is a better outline, and I think any correctness proof should follow those steps. I will remember it and use it adroitly in the exam.

Term Test

I did not do well on my term test because I did not find the correct close form for T(n) in the first question. The first question states that we only need to consider n = 2(k), so I just did the unwinding for T(2(k)) instead of T(n), and forgot to modify that n for split and recombine. Because of that mistake, I finally got a n-cube closed form and could not go on my induction proof. In a word, I got totally wrong in the first question and there are only two questions in the test. What a pity!

 Anyway, I should not be sad because there are still an assignment, a slog and a final test ahead of me. I have to work harder and harder afterwards. Also my review strategy needs to improve since I focused mostly on course notes but did not work on tutorial problems that much.

 I also went to the office hour this afternoon to ask some questions encountered in the review, for example, I did not quite understand how to solve the closest pair of dots problem.

Now I know that I should check all the dots in the neighborhood of the vertical partition line and compare those with the minimum of the left region and right region (those have already found by recursion). Moreover I got a better understanding on the multiple binary string problem.

 This week the course will be all about correctness, so I will work hard to learn it well.