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

Safe HaskellNone



Author : Levent Erkok License : BSD3 Maintainer: Stability : experimental

Demonstrates SBV's assertion checking facilities



checkedDiv :: (?loc :: CallStack) => SInt32 -> SInt32 -> SInt32 Source #

A simple variant of division, where we explicitly require the caller to make sure the divisor is not 0.

test1 :: IO [SafeResult] Source #

Check whether an arbitrary call to checkedDiv is safe. Clearly, we do not expect this to be safe:

>>> test1
[Documentation/SBV/Examples/Misc/NoDiv0.hs:36:14:checkedDiv: Divisor should not be 0: Violated. Model:
  s0 = 0 :: Int32
  s1 = 0 :: Int32]

test2 :: IO [SafeResult] Source #

Repeat the test, except this time we explicitly protect against the bad case. We have:

>>> test2
[Documentation/SBV/Examples/Misc/NoDiv0.hs:44:41:checkedDiv: Divisor should not be 0: No violations detected]