ChasingBottoms-1.3.0.6: For testing partial and infinite values.

# ChasingBottoms-1.3.0.6: For testing partial and infinite values.

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 $ filter ((== 1) . (`mod` 83)) primes)`
  `[167,499,9NonTermination`
`> timeOutMicro 100 (print $ take 6 $ filter ((== 1) . (`mod` 83)) primes)`
  `[167,499,997,1163,1993NonTermination`
`> timeOutMicro 100 (print $ take 6 $ filter ((== 1) . (`mod` 83)) primes)`
  `[167,499,997,1163,1993,2657]`
``
  `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.

Modules

- Test
  - Test.ChasingBottoms
    - Test.ChasingBottoms.Approx
    - Test.ChasingBottoms.ApproxShow
    - Test.ChasingBottoms.ContinuousFunctions
    - Test.ChasingBottoms.IsBottom
    - Test.ChasingBottoms.Nat
    - Test.ChasingBottoms.SemanticOrd
    - Test.ChasingBottoms.TimeOut