Portability | portable |
---|---|
Stability | experimental |
Maintainer | erkokl@gmail.com |
Demonstrates function counter-examples
Documentation
thmGood :: SWord8 -> SWord8 -> SWord8 -> SBoolSource
Asserts that f x z == f (y+2) z
whenever x == y+2
. Naturally correct.
thmBad :: SWord8 -> SWord8 -> SBoolSource
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 $ 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.