# ChasingBottoms

For testing partial and infinite values.

 Version on this page: 1.3.0.13 LTS Haskell 12.22: 1.3.1.5 Stackage Nightly 2018-09-28: 1.3.1.5 Latest on Hackage: 1.3.1.5

See all snapshots `ChasingBottoms` appears in

Maintained by

#### Module documentation for 1.3.0.13

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 { approxDepth = Just 5, timeOutLimit = Just 2 }
> semanticEq tweak (reverse [1..], [1..]) (bottom :: [Int], [1..] :: [Int])
True
``````
``````> let tweak = noTweak { timeOutLimit = Just 2 }
> semanticJoin tweak (reverse [1..], True) ([] :: [Int], bottom)
Just ([],True)
``````

This can of course be dangerous:

``````> let tweak = noTweak { timeOutLimit = Just 0 }
> 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.

Depends on 6 packages:
Used by 1 package: