Data.SBV.Examples.Misc.NoDiv0

Demonstrates SBV's assertion checking facilities

Documentation

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

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

test1 :: IO [SafeResult]

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

>>> test1
[Data/SBV/Examples/Misc/NoDiv0.hs:22:32:?loc,
 Data/SBV/Examples/Misc/NoDiv0.hs:37:14:checkedDiv: Divisor should not be 0: Violated. Model:
  s0 = 0 :: Int32
  s1 = 0 :: Int32]

test2 :: IO [SafeResult]

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

>>> test2
[Data/SBV/Examples/Misc/NoDiv0.hs:22:32:?loc,
 Data/SBV/Examples/Misc/NoDiv0.hs:46:41:checkedDiv: Divisor should not be 0: No violations detected]