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

Safe HaskellSafe-Infered



Demonstrates function counter-examples



f :: SWord8 -> SWord8 -> SWord16Source

An uninterpreted function

thmGood :: SWord8 -> SWord8 -> SWord8 -> SBoolSource

Asserts that f x z == f (y+2) z whenever x == y+2. Naturally correct:

>>> prove thmGood

thmBad :: SWord8 -> SWord8 -> SBoolSource

Asserts that f is commutative; which is not necessarily true! Indeed, the SMT solver returns a counter-example function that is not commutative. (Note that we have to use Yices as Z3 function counterexamples are not yet supported by sbv.) We have:

>>> proveWith yices $ forAll ["x", "y"] thmBad
Falsifiable. Counter-example:
  x = 0 :: SWord8
  y = 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.