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

Documentation.SBV.Examples.Misc.NoDiv0

Description

Demonstrates SBV's assertion checking facilities

Synopsis

# Documentation

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.

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]


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]