sbv 0.9.5 → 0.9.6

raw patch · 4 files changed

+72/−3 lines, 4 files

Files

• Data/SBV/Examples/Uninterpreted/Function.hs +42/−0
• Data/SBV/TestSuite/Uninterpreted/Function.hs +24/−0
• SBVUnitTest/SBVUnitTest.hs +3/−2
• sbv.cabal +3/−1

@@ -0,0 +1,42 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Examples.Uninterpreted.Function+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+-- Portability :  portable+--+-- Demonstrates function counter-examples+-----------------------------------------------------------------------------++module Data.SBV.Examples.Uninterpreted.Function where++import Data.SBV++-- | An uninterpreted function+f :: SWord8 -> SWord8 -> SWord16+f = uninterpret "f"++-- | Asserts that @f x z == f (y+2) z@ whenever @x == y+2@. Naturally correct.+thmGood :: SWord8 -> SWord8 -> SWord8 -> SBool+thmGood x y z = x .== y+2 ==> f x z .== f (y + 2) z++-- | Asserts that @f@ is commutative; which is not necessarily true!+-- Indeed, the SMT solver (Yices in this case) returns a counter-example+-- function that is not commutative. We have:+--+-- @+-- ghci> prove thmBad+-- Falsifiable. Counter-example:+--   s0 = 0 :: SWord8+--   s1 = 128 :: SWord8+--   -- uninterpreted: f+--        f 128 0 = 32768+--        f _ _ = 0+-- @+--+-- Note how the counterexample function @f@ returned by Yices violates commutativity;+-- thus providing evidence that the asserted theorem is not valid.+thmBad :: SWord8 -> SWord8 -> SBool+thmBad x y = f x y .== f y x

@@ -0,0 +1,24 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.TestSuite.Uninterpreted.Function+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+-- Portability :  portable+--+-- Testsuite for Data.SBV.Examples.Uninterpreted.Function+-----------------------------------------------------------------------------++module Data.SBV.TestSuite.Uninterpreted.Function where++import Data.SBV+import Data.SBV.Internals+import Data.SBV.Examples.Uninterpreted.Function++-- Test suite+testSuite :: SBVTestSuite+testSuite = mkTestSuite $ \_ -> test [+   "aufunc-0" ~: assert       =<< isTheorem thmGood+ , "aufunc-1" ~: assert . not =<< isTheorem thmBad+ ]

@@ -49,7 +49,8 @@ import qualified Data.SBV.TestSuite.Puzzles.Temperature           as T22(testSuite) import qualified Data.SBV.TestSuite.Puzzles.U2Bridge              as T23(testSuite) import qualified Data.SBV.TestSuite.Uninterpreted.AUF             as T24(testSuite)-import qualified Data.SBV.TestSuite.Uninterpreted.Uninterpreted   as T25(testSuite)+import qualified Data.SBV.TestSuite.Uninterpreted.Function        as T25(testSuite)+import qualified Data.SBV.TestSuite.Uninterpreted.Uninterpreted   as T26(testSuite)  testCollection :: [SBVTestSuite] testCollection = [@@ -59,7 +60,7 @@      , T13.testSuite, T14.testSuite, T15.testSuite, T16.testSuite      , T17.testSuite, T18.testSuite, T19.testSuite, T20.testSuite      , T21.testSuite, T22.testSuite, T23.testSuite, T24.testSuite-     , T25.testSuite+     , T25.testSuite, T26.testSuite      ] -- No user serviceable parts below.. 

@@ -1,5 +1,5 @@ Name:          sbv-Version:       0.9.5+Version:       0.9.6 Category:      Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math Synopsis:      Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers. Description:   Adds support for symbolic bit vectors, allowing formal models of bit-precise@@ -49,6 +49,7 @@                   , Data.SBV.Examples.Puzzles.Sudoku                   , Data.SBV.Examples.Puzzles.U2Bridge                   , Data.SBV.Examples.Uninterpreted.AUF+                  , Data.SBV.Examples.Uninterpreted.Function   Other-modules   : Data.SBV.BitVectors.Data                   , Data.SBV.BitVectors.Bit                   , Data.SBV.BitVectors.Model@@ -104,6 +105,7 @@                   , Data.SBV.TestSuite.Puzzles.Temperature                   , Data.SBV.TestSuite.Uninterpreted.AUF                   , Data.SBV.TestSuite.Uninterpreted.Uninterpreted+                  , Data.SBV.TestSuite.Uninterpreted.Function  Executable SBVUnitTests   main-is         : SBVUnitTest/SBVUnitTest.hs