ChasingBottoms-1.3.0: ChasingBottoms.cabal

name:               ChasingBottoms
version:            1.3.0
license:            OtherLicense
license-file:       LICENCE
copyright:          Copyright (c) Nils Anders Danielsson 2004-2010.
author:             Nils Anders Danielsson
maintainer:         http://www.cs.nott.ac.uk/~nad/contact.html
synopsis:           For testing partial and infinite values.
description:
  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.cs.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 $ 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.cs.nott.ac.uk/~nad/publications/danielsson-jansson-mpc2004.html>).
  .
  The code has been tested under GHC 6.12. Most parts can probably be
  ported to other Haskell compilers, but that would require some work.
  The @TimeOut@ functions require preemptive scheduling, and most of the
  rest requires @Data.Generics@; @isBottom@ only requires exceptions,
  though.
category:           Testing
tested-with:        GHC == 6.12.1
cabal-version:      == 1.8.*
build-type:         Simple

library
    exposed-modules:
        Test.ChasingBottoms,
        Test.ChasingBottoms.Approx,
        Test.ChasingBottoms.ApproxShow,
        Test.ChasingBottoms.ContinuousFunctions,
        Test.ChasingBottoms.IsBottom,
        Test.ChasingBottoms.Nat,
        Test.ChasingBottoms.SemanticOrd,
        Test.ChasingBottoms.TimeOut

    other-modules: Test.ChasingBottoms.IsType

    build-depends: QuickCheck == 2.1.*,
                   mtl == 1.1.*,
                   base == 4.*,
                   containers == 0.3.*,
                   random == 1.0.*,
                   syb >= 0.1.0.2 && < 0.2

flag build-tests
    description: Build the test suite.
    default:     False
    manual:      True

executable ChasingBottomsTestSuite
    if !flag(build-tests)
      buildable:   False

    main-is:       Test/ChasingBottoms/Tests.hs

    other-modules: Test.ChasingBottoms.Approx.Tests,
                   Test.ChasingBottoms.ApproxShow.Tests,
                   Test.ChasingBottoms.ContinuousFunctions.Tests,
                   Test.ChasingBottoms.IsBottom.Tests,
                   Test.ChasingBottoms.IsType.Tests,
                   Test.ChasingBottoms.Nat.Tests,
                   Test.ChasingBottoms.SemanticOrd.Tests,
                   Test.ChasingBottoms.TestUtilities,
                   Test.ChasingBottoms.TestUtilities.Generators,
                   Test.ChasingBottoms.TimeOut.Tests

    build-depends: QuickCheck == 2.1.*,
                   mtl == 1.1.*,
                   base == 4.*,
                   containers == 0.3.*,
                   random == 1.0.*,
                   syb >= 0.1.0.2 && < 0.2,
                   array == 0.3.*