No proof required; assume input correct
No proof required; assume input correct 
Assignment #4, due 25 October (Mike O'Donnell)
Proving Program?
|
Should we prove that the program works with the pre/post assertions and the invariant ... ?You don't need to write a proof. If you arrange the correspondence between preassertion, invariant, postassertion, and program right, it will be easy for me to check correctness by inspection. You might want to run through some steps of proof on your own, to check your work. I was wondering if I can informally prove the program with a flow chart?Displaying a flow chart for this program is a bad idea. If you focus your attention on reasoning about the invariant, you'll get it straight. Focusing on the flow of control leads you astray. Should we prove the termination case?You don't need to discuss termination, but you do need to make sure that your program terminates. And, termination is a bit tricky. In general, you prove termination by exhibiting a formula using the variables in the program, and showing that the value of that formula gets smaller each time through the loop, and that when it gets small enough the loop must terminate. When termination is not trivially obvious, the problem usually comes from failure to reduce the value in certain circumstances. The interesting insight in this method comes from figuring out the right formula. In the case of binary search, the formula is obvious: U-L. Different variations halt when U-L=1, 0, or -1.The only likely way of writing a nonterminating program is to get stuck repeating the next-to-last step forever. Studying the formula U-L doesn't help much in avoiding this error, since you just overlook the special cases in which your arithmetic intuition was wrong. For this particular problem, it's best to deal with termination by thinking very carefully about the cases where you appear to be one step away from termination, and make sure that you really do shrink the search region in those cases. Keep in mind that, due to the rounded division by two, you will get slightly different results depending on whether you are at an even-numbered position or an odd-numbered position. Typically, you get termination in one of those cases, but you may fail in the other.
And do we allow for user error in the input? (i.e. L > U for L= lower bound of array and U= upper bound). OR should we not allow user input on the L and U and just initialize L =0 and U = size of array?You may decide whether to let the input include L and U. I think it's slightly more elegant to do so, since it makes the input state just like the intermediate states. But it's a minor point really. In either case, you may assume that the user gives you a legitimate input, satisfying your preassertion. If you want to check the relationship between L and U that's OK but not necessary. But, it's definitely a mistake to check whether the array is sorted, since that takes much longer than the search, and makes the whole binary search technique pointless. Mike O'D. |
to: