The ChasingBottoms package

[Tags: library, mit]

Do you ever feel the need to test code involving bottoms (e.g. calls to the @error@ function), or code involving infinite values? Then this library could be useful for you.

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 (<http://www.cse.chalmers.se/~rjmh/QuickCheck/>). With this library you can do the tests as simply as the following examples show.

Testing explicitly for bottoms:

> > isBottom (head []) > True

> > isBottom bottom > True

> > isBottom (\_ -> bottom) > False

> > isBottom (bottom, bottom) > False

Comparing finite, partial values:

> > ((bottom, 3) :: (Bool, Int)) ==! (bottom, 2+5-4) > True

> > ((bottom, bottom) :: (Bool, Int)) <! (bottom, 8) > True

Showing partial and infinite values (@\\\/!@ is join and @\/\\!@ is meet):

> > approxShow 4 $ (True, bottom) \/! (bottom, 'b') > "Just (True, 'b')"

> > approxShow 4 $ (True, bottom) /\! (bottom, 'b') > "(_|_, _|_)"

> > approxShow 4 $ ([1..] :: [Int]) > "[1, 2, 3, _"

> > approxShow 4 $ (cycle [bottom] :: [Bool]) > "[_|_, _|_, _|_, _"

Approximately comparing infinite, partial values:

> > approx 100 [2,4..] ==! approx 100 (filter even [1..] :: [Int]) > True

> > approx 100 [2,4..] /=! approx 100 (filter even [bottom..] :: [Int]) > True

The code above relies on the fact that @bottom@, just as @error \"...\"@, @undefined@ 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:

> > timeOut' 1 (reverse [1..5]) > Value [5,4,3,2,1]

> > timeOut' 1 (reverse [1..]) > NonTermination

The time-out functionality can be used to treat \"slow\" computations as bottoms:

@ > let tweak = Tweak &#x7b; approxDepth = Just 5, timeOutLimit = Just 2 &#x7d; > semanticEq tweak (reverse [1..], [1..]) (bottom :: [Int], [1..] :: [Int]) True @

@ > let tweak = noTweak &#x7b; timeOutLimit = Just 2 &#x7d; > semanticJoin tweak (reverse [1..], True) ([] :: [Int], bottom) Just ([],True) @

This can of course be dangerous:

@ > let tweak = noTweak &#x7b; timeOutLimit = Just 0 &#x7d; > semanticEq tweak (reverse [1..100000000]) (bottom :: [Integer]) True @

Timeouts can also be applied to @IO@ computations:

> > let primes () = unfoldr (\(x:xs) -> Just (x, filter ((/= 0) . (`mod` x)) xs)) [2..] > > timeOutMicro 100 (print $ primes ()) > [2,NonTermination > > timeOutMicro 10000 (print $ take 10 $ primes ()) > [2,3,5,7,11,13,17,19,23,29] > Value ()

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\" (<http://www.cse.chalmers.se/~nad/publications/danielsson-jansson-mpc2004.html>).

The code has been tested using GHC. Most parts can probably be ported to other Haskell compilers, but this would require some work. The @TimeOut@ functions require preemptive scheduling, and most of the rest requires @Data.Generics@; @isBottom@ only requires exceptions, though.

Properties

Versions1.2.2, 1.2.4, 1.3.0, 1.3.0.1, 1.3.0.2, 1.3.0.3, 1.3.0.4, 1.3.0.5, 1.3.0.6, 1.3.0.7, 1.3.0.8, 1.3.0.9, 1.3.0.10, 1.3.0.11, 1.3.0.12, 1.3.0.13
Change logNone available
Dependenciesbase (>=4.0 && <4.9), containers (>=0.3 && <0.6), mtl (>=1.1 && <2.3), QuickCheck (>=2.1 && <2.9), random (>=1.0 && <1.2), syb (>=0.1.0.2 && <0.6) [details]
LicenseMIT
CopyrightCopyright (c) Nils Anders Danielsson 2004-2015.
AuthorNils Anders Danielsson
Maintainerhttp://www.cse.chalmers.se/~nad/
CategoryTesting
Source repositoryhead: darcs get http://www.cse.chalmers.se/~nad/repos/ChasingBottoms/
UploadedTue Jun 23 11:27:45 UTC 2015 by NilsAndersDanielsson
DistributionsDebian:1.3.0.13, LTSHaskell:1.3.0.13, NixOS:1.3.0.13, Stackage:1.3.0.13
Downloads4944 total (242 in last 30 days)
Votes
0 []
StatusDocs available [build log]
Last success reported on 2015-06-23 [all 1 reports]

Modules

[Index]

Downloads

Maintainers' corner

For package maintainers and hackage trustees