sbv-7.13: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Documentation.SBV.Examples.BitPrecise.BrokenSearch

Contents

- Helpers

Description

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:33:28:+!: 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.

# Helpers

checkArithOverflow :: (SInt32 -> SInt32 -> SInt32) -> IO () Source #

A helper predicate to check safety under the conditions that `low` is at least 0 and `high` is at least `low`.

checkCorrectMidValue :: (SInt32 -> SInt32 -> SInt32) -> IO ThmResult Source #

Another helper to show that the result is actually the correct value, if it was done over 64-bit integers, which is sufficiently large enough.