| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.SBV.Plugin.Examples.Maximum
Description
Shows that a naive definition of maximum doing bit-vector arithmetic is incorrect.
Documentation
myMax :: Int -> Int -> Int -> Int Source #
Compute the maximum of three integers, which is intuitively correct for unbounded values, but not for bounded bit-vectors.
correct :: Proved (Int -> Int -> Int -> Bool) Source #
Show that this function fails to compute maximum correctly. We have:
[SBV] a.hs:11:1-7 Proving "correct", using Z3. [Z3] Falsifiable. Counter-example: x = -2816883406898309583 :: Int64 y = -2816883406898309583 :: Int64 z = 6694719001794338309 :: Int64