<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!--Rendered using the Haskell Html Library v0.2-->
<HTML
><HEAD
><META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=UTF-8"
><TITLE
>Chasing Bottoms</TITLE
><LINK HREF="haddock.css" REL="stylesheet" TYPE="text/css"
><SCRIPT SRC="haddock.js" TYPE="text/javascript"
></SCRIPT
></HEAD
><BODY
><TABLE CLASS="vanilla" CELLSPACING="0" CELLPADDING="0"
><TR
><TD CLASS="topbar"
><TABLE CLASS="vanilla" CELLSPACING="0" CELLPADDING="0"
><TR
><TD
><IMG SRC="haskell_icon.gif" WIDTH="16" HEIGHT="16" ALT=" "
></TD
><TD CLASS="title"
>Chasing Bottoms</TD
><TD CLASS="topbut"
><A HREF="index.html"
>Contents</A
></TD
><TD CLASS="topbut"
><A HREF="doc-index.html"
>Index</A
></TD
></TR
></TABLE
></TD
></TR
><TR
><TD CLASS="section1"
>Chasing Bottoms</TD
></TR
><TR
><TD CLASS="doc"
><P
>Do you ever feel the need to test code involving bottoms (e.g. calls to
the <TT
>error</TT
> function), or code involving infinite values? Then this
library could be useful for you.
</P
><P
>It is usually easy to get a grip on bottoms by showing a value and
waiting to see how much gets printed before the first exception is
encountered. However, that quickly gets tiresome and is hard to automate
using e.g. QuickCheck
(<A HREF="http://www.cs.chalmers.se/~rjmh/QuickCheck/"
>http://www.cs.chalmers.se/~rjmh/QuickCheck/</A
>). With this library you
can do the tests as simply as the following examples show.
</P
><P
>Testing explicitly for bottoms:
</P
><DL
><DT
><TT
>> isBottom (head [])</TT
></DT
><DD
> <TT
>True</TT
>
</DD
><DT
><TT
>> isBottom bottom</TT
></DT
><DD
> <TT
>True</TT
>
</DD
><DT
><TT
>> isBottom (\_ -> bottom)</TT
></DT
><DD
> <TT
>False</TT
>
</DD
><DT
><TT
>> isBottom (bottom, bottom)</TT
></DT
><DD
> <TT
>False</TT
>
</DD
></DL
><P
>Comparing finite, partial values:
</P
><DL
><DT
><TT
>> ((bottom, 3) :: (Bool, Int)) ==! (bottom, 2+5-4)</TT
></DT
><DD
> <TT
>True</TT
>
</DD
><DT
><TT
>> ((bottom, bottom) :: (Bool, Int)) <! (bottom, 8)</TT
></DT
><DD
> <TT
>True</TT
>
</DD
></DL
><P
>Showing partial and infinite values (<TT
>\/!</TT
> is join and <TT
>/\!</TT
> is meet):
</P
><DL
><DT
><TT
>> approxShow 4 $ (True, bottom) \/! (bottom, 'b')</TT
></DT
><DD
> <TT
>"Just (True, 'b')"</TT
>
</DD
><DT
><TT
>> approxShow 4 $ (True, bottom) /\! (bottom, 'b')</TT
></DT
><DD
> <TT
>"(_|_, _|_)"</TT
>
</DD
><DT
><TT
>> approxShow 4 $ ([1..] :: [Int])</TT
></DT
><DD
> <TT
>"[1, 2, 3, _"</TT
>
</DD
><DT
><TT
>> approxShow 4 $ (cycle [bottom] :: [Bool])</TT
></DT
><DD
> <TT
>"[_|_, _|_, _|_, _"</TT
>
</DD
></DL
><P
>Approximately comparing infinite, partial values:
</P
><DL
><DT
><TT
>> approx 100 [2,4..] ==! approx 100 (filter even [1..] :: [Int])</TT
></DT
><DD
> <TT
>True</TT
>
</DD
><DT
><TT
>> approx 100 [2,4..] /=! approx 100 (filter even [bottom..] :: [Int])</TT
></DT
><DD
> <TT
>True</TT
>
</DD
></DL
><P
>The code above relies on the fact that <TT
>bottom</TT
>, just as <TT
>error
"..."</TT
>, <TT
>undefined</TT
> and pattern match failures, yield
exceptions. Sometimes we are dealing with properly non-terminating
computations, such as the following example, and then it can be nice to
be able to apply a time-out:
</P
><DL
><DT
><TT
>> timeOut' 1 (reverse [1..5]) >>= print</TT
></DT
><DD
> <TT
>Value [5,4,3,2,1]</TT
>
</DD
><DT
><TT
>> timeOut' 1 (reverse [1..]) >>= print</TT
></DT
><DD
> <TT
>NonTermination</TT
>
</DD
></DL
><P
>The time-out functionality can be used to treat "slow" computations as
bottoms:
</P
><DL
><DT
><TT
>> let tweak = Tweak { approxDepth = Just 5, timeOutLimit = Just 2 }</TT
></DT
><DD
>
</DD
><DT
><TT
>> semanticEq tweak (reverse [1..], [1..]) (bottom :: [Int], [1..] :: [Int])</TT
></DT
><DD
> <TT
>True</TT
>
</DD
><DT
><TT
>> let tweak = noTweak { timeOutLimit = Just 2 }</TT
></DT
><DD
>
</DD
><DT
><TT
>> semanticJoin tweak (reverse [1..], True) ([] :: [Int], bottom)</TT
></DT
><DD
> <TT
>Just ([],True)</TT
>
</DD
></DL
><P
>This can of course be dangerous:
</P
><DL
><DT
><TT
>> let tweak = noTweak { timeOutLimit = Just 0 }</TT
></DT
><DD
>
</DD
><DT
><TT
>> semanticEq tweak (reverse [1..100000000]) (bottom :: [Integer])</TT
></DT
><DD
> <TT
>True</TT
>
</DD
></DL
><P
>Timeouts can also be applied to <TT
>IO</TT
> computations:
</P
><DL
><DT
><TT
>> let primes = unfoldr (\(x:xs) -> Just (x, filter ((/= 0) . (`mod` x)) xs)) [2..]</TT
></DT
><DD
>
</DD
><DT
><TT
>> timeOutMicro 100 (print $ filter ((== 1) . (`mod` 83)) primes) >>= print</TT
></DT
><DD
> <TT
>[167,499NonTermination</TT
>
</DD
><DT
><TT
>> timeOutMicro 100 (print $ take 4 $ filter ((== 1) . (`mod` 83)) primes) >>= print</TT
></DT
><DD
> <TT
>[167,499,997NonTermination</TT
>
</DD
><DT
><TT
>> timeOutMicro 100 (print $ take 4 $ filter ((== 1) . (`mod` 83)) primes) >>= print</TT
></DT
><DD
> <TT
>[167,499,997,1163]</TT
>
</DD
><DT
><TT
> </TT
></DT
><DD
> <TT
>Value ()</TT
>
</DD
></DL
><P
>All the type annotations above are required.
</P
><P
>For the underlying theory and a larger example involving use of
QuickCheck, see the article "Chasing Bottoms, A Case Study in Program
Verification in the Presence of Partial and Infinite Values"
(<A HREF="http://www.cs.chalmers.se/~nad/publications/danielsson-jansson-mpc2004.html"
>http://www.cs.chalmers.se/~nad/publications/danielsson-jansson-mpc2004.html</A
>).
</P
><P
>The code has been tested under GHC 6.8. Most parts can probably be
ported to other Haskell compilers, but that would require some work.
The <TT
>TimeOut</TT
> functions require preemptive scheduling, and most of the
rest requires <TT
>Data.Generics</TT
>; <TT
>isBottom</TT
> only requires exceptions,
though.
</P
><P
>Source code: <A HREF="http://www.cs.chalmers.se/~nad/software/ChasingBottoms/ChasingBottoms.tar.gz"
>http://www.cs.chalmers.se/~nad/software/ChasingBottoms/ChasingBottoms.tar.gz</A
>.
</P
></TD
></TR
><TR
><TD CLASS="section1"
>Modules</TD
></TR
><TR
><TD
><TABLE CLASS="vanilla2" CELLSPACING="0" CELLPADDING="0"
><TR
><TD STYLE="width: 50em"
><IMG SRC="minus.gif" CLASS="coll" ONCLICK="toggle(this,'n:0')" ALT="show/hide"
>Test</TD
><TD
></TD
><TD
></TD
></TR
><TR
><TD STYLE="padding: 0; padding-left: 2em" COLSPAN="3"
><TABLE CLASS="vanilla2" CELLSPACING="0" CELLPADDING="0" ID="n:0" STYLE="display:block;"
><TR
><TD STYLE="width: 48em"
><IMG SRC="minus.gif" CLASS="coll" ONCLICK="toggle(this,'n:1')" ALT="show/hide"
><A HREF="Test-ChasingBottoms.html"
>Test.ChasingBottoms</A
></TD
><TD
></TD
><TD
></TD
></TR
><TR
><TD STYLE="padding: 0; padding-left: 2em" COLSPAN="3"
><TABLE CLASS="vanilla2" CELLSPACING="0" CELLPADDING="0" ID="n:1" STYLE="display:block;"
><TR
><TD STYLE="padding-left: 1.25em;width: 46em"
><A HREF="Test-ChasingBottoms-Approx.html"
>Test.ChasingBottoms.Approx</A
></TD
><TD
></TD
><TD
></TD
></TR
><TR
><TD STYLE="padding-left: 1.25em;width: 46em"
><A HREF="Test-ChasingBottoms-ApproxShow.html"
>Test.ChasingBottoms.ApproxShow</A
></TD
><TD
></TD
><TD
></TD
></TR
><TR
><TD STYLE="padding-left: 1.25em;width: 46em"
><A HREF="Test-ChasingBottoms-ContinuousFunctions.html"
>Test.ChasingBottoms.ContinuousFunctions</A
></TD
><TD
></TD
><TD
></TD
></TR
><TR
><TD STYLE="padding-left: 1.25em;width: 46em"
><A HREF="Test-ChasingBottoms-IsBottom.html"
>Test.ChasingBottoms.IsBottom</A
></TD
><TD
></TD
><TD
></TD
></TR
><TR
><TD STYLE="padding-left: 1.25em;width: 46em"
><A HREF="Test-ChasingBottoms-Nat.html"
>Test.ChasingBottoms.Nat</A
></TD
><TD
></TD
><TD
></TD
></TR
><TR
><TD STYLE="padding-left: 1.25em;width: 46em"
><A HREF="Test-ChasingBottoms-SemanticOrd.html"
>Test.ChasingBottoms.SemanticOrd</A
></TD
><TD
></TD
><TD
></TD
></TR
><TR
><TD STYLE="padding-left: 1.25em;width: 46em"
><A HREF="Test-ChasingBottoms-TimeOut.html"
>Test.ChasingBottoms.TimeOut</A
></TD
><TD
></TD
><TD
></TD
></TR
></TABLE
></TD
></TR
></TABLE
></TD
></TR
></TABLE
></TD
></TR
><TR
><TD CLASS="s15"
></TD
></TR
><TR
><TD CLASS="botbar"
>Produced by <A HREF="http://www.haskell.org/haddock/"
>Haddock</A
> version 0.7</TD
></TR
></TABLE
></BODY
></HTML
>