I'm tempted to solve it with:
low/2 + high/2 + (low & high & 1);
Nearly all binary search and merge sort implementations are broken (2006)
11–20 of 70 posts
Re: Nearly all binary search and merge sort implementations are broken (2006)
#12This bug requires either (1) low/mid/high are pointers [edit - I don't think this is valid; IIRC pointer arithmetic is only sane for add/subtract an int from a pointer, not divide a pointer or add two pointers]; or (2) item_count > INT_MAX / 2, which means memory_size >= sizeof(your_array) == sizeof(item) * item_count > INT_MAX / 2, which means either 1-byte or 2-byte array elements, or that your ints are smaller tha…
You can also substract two pointers (this is defined only if the two pointers are within a common memory area). The result is a ptrdiff_t which is more or less the scalar version of a void*.
Re: Nearly all binary search and merge sort implementations are broken (2006)
#13This bug requires either (1) low/mid/high are pointers [edit - I don't think this is valid; IIRC pointer arithmetic is only sane for add/subtract an int from a pointer, not divide a pointer or add two pointers]; or (2) item_count > INT_MAX / 2, which means memory_size >= sizeof(your_array) == sizeof(item) * item_count > INT_MAX / 2, which means either 1-byte or 2-byte array elements, or that your ints are smaller tha…
The author is claiming that nearly all binary search implementations are wrong under those specific conditions, not that binary search implementations are wrong under nearly all conditions.
Re: Nearly all binary search and merge sort implementations are broken (2006)
#14It 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…
"Beware of bugs in the above code; I have only proved it correct, not tried it."
— Donald KnuthRe: Nearly all binary search and merge sort implementations are broken (2006)
#15It 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…
You can prove the correctness of a program given a specification of the language you write it in. But is the compiler you use to compile your program correct? Do you know all processor bugs?
Computer hardware is not correct. So, you need to step past mathematical perfection and write defensively.
Rule 1: you can't trust RAM it lies.
That said you can build automated tests that add random memory errors to help find the program that's best able to handle memory errors.
Re: Nearly all binary search and merge sort implementations are broken (2006)
#16It 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…
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. But in practice, it's easy to make a simple mistake in implementation and accidentally throw your proof out the window. The proof remains valid, but your implementation isn't doing what the proof says.
The fact that a famous book on proving correct and then implementing a binary search ended up being slightly wrong underscores how easy it is to make this mistake. (I find binary search a little annoying because of the integer division. Do you round up or round down? What does your language implementation do? Now you see why you need to mentally prove that you've written the right algorithm, and then test to make sure your computer is doing what you think you're telling it to.)
Re: Nearly all binary search and merge sort implementations are broken (2006)
#17It 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…
> 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 e.g. Haskell is purely functional, and your representation e.g. data types is faithful to the algorithm, then you can make claims about your provably correct implementation.
Re: Nearly all binary search and merge sort implementations are broken (2006)
#18Bypass the borked formatting (original is JS dependent; link below is to Google text-only cache): http://webcache.googleusercontent.com/search?strip=1&q=c... IIRC, this made the rounds a few years ago, in case it sounds familiar.
Thanks. The site is so broken on the ipad, asks if you want a static view which goes to the front page, or an "unsupported" dynamic view which actually turns out to work and is the same page. Google this is so broken! Just make html that works in a browser!
Re: Nearly all binary search and merge sort implementations are broken (2006)
#19It 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…
You can prove the correctness of a program given a specification of the language you write it in. But is the compiler you use to compile your program correct? Do you know all processor bugs?
I have heard from someone involved with project management of military aircraft software that the process includes verification of machine code produced by the compiler, that is: you have to prove that the code generated is exactly what you intended to get.
http://www.sandroid.org/birdsproject/4dummies.html gives a glimpse of how much fun developing software for aviation purposes is.
Re: Nearly all binary search and merge sort implementations are broken (2006)
#20It 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…
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 to the contrary, either in your comment or in the above article and that same implementation described works perfectly in Python.