ChasingBottoms-1.3.1.9: For testing partial and infinite values.

# ChasingBottoms-1.3.1.9: 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 $ 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.

Signatures

Modules

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