Documentation.SBV.Examples.Misc.NoDiv0

Author : Levent Erkok License : BSD3 Maintainer: [e-mail] Stability : experimental

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
[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]

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]