4 ms·

> 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.

• feral 10y ago
  '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.
  • cmdrfred 10y ago
    > because writing out every like 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?
    • tinco 10y ago
      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.
• mnarayan01 10y ago
  On an idealized machine with arbitrarily large integers I assume.
  • haimez 10y ago
    How else do you "prove" trivial algorithms other than by removing the realities of an actual runtime environment? 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.
    • mnarayan01 10y ago
      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.
      • haimez 10y ago
        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.
  • mark-r 10y ago
    This is why I prefer to use Python for my binary searches ;-)
• mshenfield 10y ago
  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.
• Tloewald 10y ago
  A proof is only, at bottom, a convincing argument. Mathmematicians are harder to convince than most people, but they can still miss things.