/usr/share/doc/libghc-sbv-doc/html/Data-SBV-Examples-Misc-NoDiv0.html

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Data.SBV.Examples.Misc.NoDiv0</title><link href="ocean.css" rel="stylesheet" type="text/css" title="Ocean" /><script src="haddock-util.js" type="text/javascript"></script><script src="file:///usr/share/javascript/mathjax/MathJax.js" type="text/javascript"></script><script type="text/javascript">//<![CDATA[
window.onload = function () {pageLoad();setSynopsis("mini_Data-SBV-Examples-Misc-NoDiv0.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Data-SBV-Examples-Misc-NoDiv0.html">Source</a></li><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul><p class="caption">sbv-5.14: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.</p></div><div id="content"><div id="module-header"><table class="info"><tr><th valign="top">Copyright</th><td>(c) Levent Erkok</td></tr><tr><th>License</th><td>BSD3</td></tr><tr><th>Maintainer</th><td>erkokl@gmail.com</td></tr><tr><th>Stability</th><td>experimental</td></tr><tr><th>Safe Haskell</th><td>None</td></tr><tr><th>Language</th><td>Haskell2010</td></tr></table><p class="caption">Data.SBV.Examples.Misc.NoDiv0</p></div><div id="description"><p class="caption">Description</p><div class="doc"><p>Demonstrates SBV's assertion checking facilities</p></div></div><div id="synopsis"><p id="control.syn" class="caption expander" onclick="toggleSection('syn')">Synopsis</p><ul id="section.syn" class="hide" onclick="toggleSection('syn')"><li class="src short"><a href="#v:checkedDiv">checkedDiv</a> :: (?loc :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/GHC-Stack.html#t:CallStack">CallStack</a>) =&gt; <a href="Data-SBV-Internals.html#t:SInt32">SInt32</a> -&gt; <a href="Data-SBV-Internals.html#t:SInt32">SInt32</a> -&gt; <a href="Data-SBV-Internals.html#t:SInt32">SInt32</a></li><li class="src short"><a href="#v:test1">test1</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/System-IO.html#t:IO">IO</a> [<a href="Data-SBV.html#t:SafeResult">SafeResult</a>]</li><li class="src short"><a href="#v:test2">test2</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/System-IO.html#t:IO">IO</a> [<a href="Data-SBV.html#t:SafeResult">SafeResult</a>]</li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><a id="v:checkedDiv" class="def">checkedDiv</a> :: (?loc :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/GHC-Stack.html#t:CallStack">CallStack</a>) =&gt; <a href="Data-SBV-Internals.html#t:SInt32">SInt32</a> -&gt; <a href="Data-SBV-Internals.html#t:SInt32">SInt32</a> -&gt; <a href="Data-SBV-Internals.html#t:SInt32">SInt32</a> <a href="src/Data-SBV-Examples-Misc-NoDiv0.html#checkedDiv" class="link">Source</a> <a href="#v:checkedDiv" class="selflink">#</a></p><div class="doc"><p>A simple variant of division, where we explicitly require the
 caller to make sure the divisor is not 0.</p></div></div><div class="top"><p class="src"><a id="v:test1" class="def">test1</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/System-IO.html#t:IO">IO</a> [<a href="Data-SBV.html#t:SafeResult">SafeResult</a>] <a href="src/Data-SBV-Examples-Misc-NoDiv0.html#test1" class="link">Source</a> <a href="#v:test1" class="selflink">#</a></p><div class="doc"><p>Check whether an arbitrary call to <code><a href="Data-SBV-Examples-Misc-NoDiv0.html#v:checkedDiv">checkedDiv</a></code> is safe. Clearly, we do not expect
 this to be safe:</p><pre class="screen"><code class="prompt">&gt;&gt;&gt; </code><strong class="userinput"><code>test1
</code></strong>[Data/SBV/Examples/Misc/NoDiv0.hs:36:14:checkedDiv: Divisor should not be 0: Violated. Model:
  s0 = 0 :: Int32
  s1 = 0 :: Int32]
</pre></div></div><div class="top"><p class="src"><a id="v:test2" class="def">test2</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/System-IO.html#t:IO">IO</a> [<a href="Data-SBV.html#t:SafeResult">SafeResult</a>] <a href="src/Data-SBV-Examples-Misc-NoDiv0.html#test2" class="link">Source</a> <a href="#v:test2" class="selflink">#</a></p><div class="doc"><p>Repeat the test, except this time we explicitly protect against the bad case. We have:</p><pre class="screen"><code class="prompt">&gt;&gt;&gt; </code><strong class="userinput"><code>test2
</code></strong>[Data/SBV/Examples/Misc/NoDiv0.hs:44:41:checkedDiv: Divisor should not be 0: No violations detected]
</pre></div></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.17.3</p></div></body></html>
libghc-sbv-doc 5.14-1build3 / usr / share / doc / libghc-sbv-doc / html / Data-SBV-Examples-Misc-NoDiv0.html
