We were looking at Quicksort today in Algorithms. The proof that the partition step (which is the only step that actually does anything) works relied on the standard tricks for proving loop functions: establish some loop invariants for the base case and then inductively show they hold for other cases. It wasn't intended to be a super-formal proof, but it did have a pretty big hole in it. Basically, one of the steps assumed that both partitions were non-empty. That will never be the case after the first loop (since the first item can only go into one of the partitions) and it may never be the case since terminating with an empty partition is a valid end case.
Now, I know Quicksort works, and it wouldn't have been enlightening to cover extra cases to handle when only 1 partition has an item. So, I kept my mouth shut and let the class move on. However, I do think that it drives home one of the problems with formal proofs of correctness. Edge cases are the undoing of so many algorithms. Yet, it is very easy to put together a convincing proof that fails to account for them. I don't think good QA practices will be going away any time soon.
No comments:
Post a Comment