Not in java (arrays can only be indexed by a signed 32 bit integer) and the C++ solution works exactly the same way with the full 64 bit data types. That much should be obvious, and if you think you might legitimately exceed two billion elements in the array you're sorting- you'd be a fool to rely on someone else's sort implementation.
> I was shocked to learn that the binary search program that Bentley proved correct and subsequently tested in Chapter 5 of Programming Pearls contains a bug.
'Proofs' done by humans are done within a certain context; there's usually a lot that goes unstated, or is left unexamined at the finest level of detail.
Generally that isn't a problem and the 'small' details or assumptions don't 'leak' up to higher levels and do any real damage to the proof.
There's a movement to make proofs formally verified, to try move towards eliminating this issue, but that's hard, because writing out every little detail, specifying every last piece of context & assumption & step is laborious.
It is not the verification that is laborious, although it can be computationally intensive, it is the specification. It is making sure that whatever it is you are proving is actually exactly and completely what you desire of the function.
In this case the proof did not properly account for the full range of inputs, of at least skipped over the fact that in real hardware the integer domains are finite.
There's a lot of formal verification tools out there though, they do make it easier,easy enough to at least properly verify the correctness of a simple sorting algorithm.
If you sufficiently specify the runtime environment the proof can still work: Since the array is composed of integers, many C compilers/machine architectures will dictate a maximum size of the array s.t. there can't be overflow.
Touche, and fair enough- although you would expect them to call out that limitation since it's both critical and highly un-general. Bytes are comparable, small, and common enough to at least accommodate an exclusionary statement in the proof.
One possible scenario is he proved it correct assuming that the ints in the function were mathematical integers(-infinity, ... -1, 0, 1, ..., infinity). In realty all representations of numbers have an upper limit after which the representation will become corrupted or unsupported.
But the goal is only to work for the finite number of possible inputs allowed by the input types. There's no reason a finite machine has to fail on those.
It's not impossible to guarantee that a system has sufficient memory for all possible inputs. Look at high stakes embedded software development. You need more control than you get as an application on a desktop computer but there's nothing inherent about finite state machines that make them vulnerable.
Yep, this is just vintage click-bait.. you can bet more than sorting routines will fail with numbers approaching 2^63. It doesn't matter because if you're running quick sort on a list of 2^64 entries then something else is going wrong before your (l+r)/2 has a chance to overflow.
int in Java and C is 32 bit wide, not 64 bit, this limit is easily reached.
You cannot just assume nobody will use your algorithms with large inputs and act like your data types have unlimited range. Such bugs will typically manifest at important customers and be hard to analyze. Better think about your types beforehand and do add runtime checks!
At the risk of sounding stupid, I had a question about the following solution:
int mid = (low + high) >>> 1;
I understand that right shift is like dividing by 2, just like in decimal right shifting the digits is like dividing by 10 (654/10 = 065). But why can we just ignore the low + high overflow issue? Is it because the overflow will be stored in the two's complement bit and right shift doesn't care about what that bit represents? If unsigned ints were used instead, I suppose that trick wouldn't work?
low and high are assumed to be positive and at most 2^31 - 1. So, there is a zeroed high bit in each which, for a signed int, is reserved to indicate negation.
When low and hi are summed together, the high bit of the result might be set. For a signed int, this would be an accidental overflow and would be falsely interpreted as a negative number. However, if you interpret the result as an unsigned int, it would be the correct sum.
The Java logical shift operator >>> does not retain the sign when shifting. So, it will always shift a 0 into the high bit, making the result a positive signed int.
In most C implementations, >> is an arithmetic shift, which would retain the sign in the result. So in C, we would need to cast low and high as unsigned first; otherwise, the high bit will be retained rather than shifted.
A more interesting version of that bug, I find, and the reason why I almost never used unsigned values in my algorithm is that when you compute indices in a non-trivial way, any intermediate value that is negative will break your program.
Here's another approach: represent the range as a (low, length) pair instead of (low, high). The update becomes either length /= 2 or low += length/2, length -= length/2. IIRC this was what I did when I adapted Bentley's code to C 25 years ago, mainly because of overflow. It never occurred to me to check if standard libraries got it wrong.
35 comments
[ 2.1 ms ] story [ 87.2 ms ] threadAs to C++ 2+ billion byte arrays are not uncommon. It's just a few gigs of ram for int[] arrays.
Huh? How did he prove it correct, then?
Generally that isn't a problem and the 'small' details or assumptions don't 'leak' up to higher levels and do any real damage to the proof.
There's a movement to make proofs formally verified, to try move towards eliminating this issue, but that's hard, because writing out every little detail, specifying every last piece of context & assumption & step is laborious.
Can code be written and subsequently formally verified that can then help in the process of formally verifying code?
In this case the proof did not properly account for the full range of inputs, of at least skipped over the fact that in real hardware the integer domains are finite.
There's a lot of formal verification tools out there though, they do make it easier,easy enough to at least properly verify the correctness of a simple sorting algorithm.
I'm pretty sure you're right though. Integers must have been defined as infinite in the proof for it to have been a proof at all.
You cannot just assume nobody will use your algorithms with large inputs and act like your data types have unlimited range. Such bugs will typically manifest at important customers and be hard to analyze. Better think about your types beforehand and do add runtime checks!
A function, especially when part of the standard library, must work correctly for all possible inputs or reject them outright.
[1] https://news.ycombinator.com/item?id=12146049
At the risk of sounding stupid, I had a question about the following solution:
I understand that right shift is like dividing by 2, just like in decimal right shifting the digits is like dividing by 10 (654/10 = 065). But why can we just ignore the low + high overflow issue? Is it because the overflow will be stored in the two's complement bit and right shift doesn't care about what that bit represents? If unsigned ints were used instead, I suppose that trick wouldn't work?When low and hi are summed together, the high bit of the result might be set. For a signed int, this would be an accidental overflow and would be falsely interpreted as a negative number. However, if you interpret the result as an unsigned int, it would be the correct sum.
The Java logical shift operator >>> does not retain the sign when shifting. So, it will always shift a 0 into the high bit, making the result a positive signed int.
In most C implementations, >> is an arithmetic shift, which would retain the sign in the result. So in C, we would need to cast low and high as unsigned first; otherwise, the high bit will be retained rather than shifted.
Why not simply
Here's another approach: represent the range as a (low, length) pair instead of (low, high). The update becomes either length /= 2 or low += length/2, length -= length/2. IIRC this was what I did when I adapted Bentley's code to C 25 years ago, mainly because of overflow. It never occurred to me to check if standard libraries got it wrong.
No, this just indicates that you didn't prove it rigorously enough :p
Why this instead of the more intuitive `low/2 + high/2` ?
Edit: Nevermind, I get it. The reason is instructive: In the case where high and low are odd numbers, the "more intuitive" way is off by one.