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

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.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.

test1 :: IO [SafeResult] Source #

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: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
[Data/SBV/Examples/Misc/NoDiv0.hs:44:41:checkedDiv: Divisor should not be 0: No violations detected]