While true, it seems that if your array is that close to the inherent size limit in indexing by ints, this is at most a temporary fix. How fast does your sorting requirements go from 2^31 to 2^32? It seems that you should be using size_t here, not int.
size_t is actually 32-bit on some 64-bit platforms; you want uint64_t.
Nearly all binary search and merge sort implementations are broken (2006)
41–50 of 70 posts
Re: Nearly all binary search and merge sort implementations are broken (2006)
#42An interesting article that links back to this one: http://reprog.wordpress.com/2010/04/19/are-you-one-of-the-10... The claim is that even ignoring overflow, only 10% of programmers can correctly implement a binary search. When I tried it, I thought I got it working, but it was later pointed out that I didn't handle empty lists correctly. Programming correctly is hard.
Couldn't resist that challenge (although the thread is nearly 2 years old.) I think mine works, at least it gives the right answer for all my test cases.
Re: Nearly all binary search and merge sort implementations are broken (2006)
#43So C, C++, and Java don't have good support for arithmetic. What else is new?
Re: Nearly all binary search and merge sort implementations are broken (2006)
#44Nice to see that the Go gets it right: func Search(n int, f func(int) bool) int { // Define f(-1) == false and f(n) == true. // Invariant: f(i-1) == false, f(j) == true. i, j := 0, n for i answer is i. return i } http://code.google.com/p/go/source/browse/src/pkg/sort/searc...
Re: Nearly all binary search and merge sort implementations are broken (2006)
#45I'm tempted to suggest that the fixed C/C++ version is still not correct with respect to this issue, namely on architectures where INT_MAX == UINT_MAX. (Or really INT_MAX = 65535.)
INT_MAX == UINT_MAX is the only valid failing case, because elsewhere in the standard integer types are restricted to pure binary representations. This means that if UINT_MAX is greater than INT_MAX, it must be at least INT_MAX * 2 + 1.
http://groups.google.com/group/comp.std.c/browse_thread/thre...
Re: Nearly all binary search and merge sort implementations are broken (2006)
#46Earlier quoted context omitted.
Mathematics sits atop a very small set of trusted axioms. Computer hardware is not so reliable; the parts are made in China as cheaply as possible. So even if you've proven something correct in theory, it doesn't matter because of all the additional variables that the real world introduces. The big insights in computer science look very much like mathematics; the mechanics of a binary search work perfectly in theory.…
Actually most bugs are being introduced in the translation between pseudocode and your working programming language. For instance pseudocode does not deal with 32-bit integers that can overflow. But that's not the fault of the algorithm, or the fault of its proof and it also has nothing to do with the origin of your computer parts. Also, the "mechanics" of binary search work perfectly in practice. I see no evidence t…
Re: Nearly all binary search and merge sort implementations are broken (2006)
#47It is not sufficient merely to prove a program correct; you have to test it too. Moreover, to be really certain that a program is correct, you have to test it for all possible input values, but this is seldom feasible. This statement is tantamount to saying "you don't merely need to prove Fermat's Last Theorem, you also have to test it for all possible input values". By this line of reasoning, most of mathematics sho…
How do you prove the proof is correct? And how do you prove that your mathematical representation correctly corresponds to the problem you are modeling? This is why I am bitter and disillusioned about mathematics: it promises certainty, but doesn't deliver. It remains pragmatically useful, like many other tools, but does not deserve the semi-mystical status some confer on it.
Re: Nearly all binary search and merge sort implementations are broken (2006)
#48It is not sufficient merely to prove a program correct; you have to test it too. Moreover, to be really certain that a program is correct, you have to test it for all possible input values, but this is seldom feasible. This statement is tantamount to saying "you don't merely need to prove Fermat's Last Theorem, you also have to test it for all possible input values". By this line of reasoning, most of mathematics sho…
How do you prove the proof is correct? And how do you prove that your mathematical representation correctly corresponds to the problem you are modeling? This is why I am bitter and disillusioned about mathematics: it promises certainty, but doesn't deliver. It remains pragmatically useful, like many other tools, but does not deserve the semi-mystical status some confer on it.
Everything can be proved to be "correct", for some definition of "correct" (i.e. "output undefined, program may not terminate").
Re: Nearly all binary search and merge sort implementations are broken (2006)
#49Earlier quoted context omitted.
> This statement is tantamount to saying "you don't merely need to prove Fermat's Last Theorem, you also have to test it for all possible input values". By this line of reasoning, most of mathematics should be thrown out. > If you've proven a program correct .. You are making a categorical error: One proves algorithms and tests programs. A program is a representation of an algorithm. If the language of implementation…
You are making a categorical error: One proves algorithms and tests programs. You can prove programs too, not just algorithms. That's what the entire (exorbitantly expensive) field of verified applications lies upon. Even my college class on formal logic covered the basics of this, and there's billions of dollars worth of extremely high-reliability applications that have been developed using such formal proofs. For e…
The way this usually works is that the proof is written and the code is then generated from the proof. That code is then incorporated in something larger, which has not been proven correct. Such is the case with algorithms. You can mathematically prove an algorithm correct. You can even write a proof and generate a program from it. Then you still have to use that algorithm and all the code using it can't be proven correct with current methods. That is why you will still have to test your program.
There are even entire programming languages designed for
the sole purpose of making formal, mathematical
verification of programs easier.
Yes, and their practical usefulness is still severely limited.[1] Of course, in theory this means they can deal with any data; in practice it means they can't.
Re: Nearly all binary search and merge sort implementations are broken (2006)
#50Earlier quoted context omitted.
Actually most bugs are being introduced in the translation between pseudocode and your working programming language. For instance pseudocode does not deal with 32-bit integers that can overflow. But that's not the fault of the algorithm, or the fault of its proof and it also has nothing to do with the origin of your computer parts. Also, the "mechanics" of binary search work perfectly in practice. I see no evidence t…
Upvoted for the first two paragraphs, but I can't make sense of the second sentence of the third paragraph. The algorithm given in the article works in Python because Python has different overflow behavior than Java, C, or C++. When you say you "see no evidence", it seems like you are saying the implementation given in the article does work in Java etc.