Copyright | (c) Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
The classic "binary-searches are broken" example: http://ai.googleblog.com/2006/06/extra-extra-read-all-about-it-nearly.html
Synopsis
- midPointBroken :: SInt32 -> SInt32 -> SInt32
- midPointFixed :: SInt32 -> SInt32 -> SInt32
- midPointAlternative :: SInt32 -> SInt32 -> SInt32
- checkArithOverflow :: (SInt32 -> SInt32 -> SInt32) -> IO ()
- checkCorrectMidValue :: (SInt32 -> SInt32 -> SInt32) -> IO ThmResult
Documentation
midPointBroken :: SInt32 -> SInt32 -> SInt32 Source #
Model the mid-point computation of the binary search, which is broken due to arithmetic overflow. Note how we use the overflow checking variants of the arithmetic operators. We have:
>>>
checkArithOverflow midPointBroken
Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs:35:32:+!: SInt32 addition overflows: Violated. Model: low = 2147483647 :: Int32 high = 2147483647 :: Int32
Indeed:
>>>
(2147483647 + 2147483647) `div` (2::Int32)
-1
giving us a negative mid-point value!
midPointFixed :: SInt32 -> SInt32 -> SInt32 Source #
The correct version of how to compute the mid-point. As expected, this version doesn't have any underflow or overflow issues:
>>>
checkArithOverflow midPointFixed
No violations detected.
As expected, the value is computed correctly too:
>>>
checkCorrectMidValue midPointFixed
Q.E.D.
midPointAlternative :: SInt32 -> SInt32 -> SInt32 Source #
Show that the variant suggested by the blog post is good as well:
mid = ((unsigned int)low + (unsigned int)high) >> 1;
In this case the overflow is eliminated by doing the computation at a wider range:
>>>
checkArithOverflow midPointAlternative
No violations detected.
And the value computed is indeed correct:
>>>
checkCorrectMidValue midPointAlternative
Q.E.D.