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.
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.
No comments:
Post a Comment