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

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Documentation.SBV.Examples.Misc.NoDiv0

Description

Demonstrates SBV's assertion checking facilities

Synopsis

- checkedDiv :: (?loc :: CallStack) => SInt32 -> SInt32 -> SInt32
- test1 :: IO [SafeResult]
- test2 :: IO [SafeResult]

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