Proving program correctness is always an annoying part, especially dealing with searching items and sorting items in an array or list. There are many conditions to consider for the program(most of them we have seen during this week were recursive programs) correctness.
The proof of correctness may be like: by induction, for size of the input,
prove precondition -> termination&postcondition. It seems the structure of
complete induction is well following recursive structure.
Then we go through the first few lines and if lucky enough we can proceed to the
annoying part of the recursive function. In this case, the recursive step leads us
to examine the whole function again with different input size, a smaller size.
We don't stop checking until we get the expected result - the post condition.
But how to split up the size so that it will look more straightforward and easier to
be checked? For the binary search, the way is to break into the middle of a list.
So there may be various ways and algorithms for various problems to shrink the
searching or sorting range. The next thing is to continue on executing. The case
must be carefully chosen otherwise some unexpected errors may cause the crush
of the program.
The proof is complicated at most of the time so as to ensure all the codes work from the
first line with the initial input. It saves us a lot of time to complement any cases or to fix
up any mistakes afterwards.
No comments:
Post a Comment