[Made it possible to build the documentation using cabal-install. Nils Anders Danielsson **20080318173646 + Removed the docs and dist targets from the makefile. ] { hunk ./ChasingBottoms.cabal 12 -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. +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 + (). 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)) 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\]) >>= print@] @Value [5,4,3,2,1]@ + . + [@> timeOut' 1 (reverse [1..\]) >>= print@] @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) >>= print@] @[167,499NonTermination@ + . + [@> timeOutMicro 100 (print $ take 4 $ filter ((== 1) . (\`mod\` 83)) primes) >>= print@] @[167,499,997NonTermination@ + . + [@> timeOutMicro 100 (print $ take 4 $ filter ((== 1) . (\`mod\` 83)) primes) >>= print@] @[167,499,997,1163]@ + . + [@ @] @Value ()@ + . + All the type annotations above are required. + . + 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\" + (). + . + The code has been tested under GHC 6.8. 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. + . + Source code: . hunk ./Header 1 -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 -(). 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)) 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\]) >>= print@] @Value [5,4,3,2,1]@ - - [@> timeOut' 1 (reverse [1..\]) >>= print@] @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) >>= print@] @[167,499NonTermination@ - - [@> timeOutMicro 100 (print $ take 4 $ filter ((== 1) . (\`mod\` 83)) primes) >>= print@] @[167,499,997NonTermination@ - - [@> timeOutMicro 100 (print $ take 4 $ filter ((== 1) . (\`mod\` 83)) primes) >>= print@] @[167,499,997,1163]@ - - [@ @] @Value ()@ - -All the type annotations above are required. - -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\" -(). - -The code has been tested under GHC 6.8. 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. - -Source code: . rmfile ./Header hunk ./Makefile 1 -# This Makefile is currently only used to build the documentation and -# to run a test suite automatically using darcs. +# This Makefile is currently only used to run a test suite +# automatically using darcs. hunk ./Makefile 7 -# Path to Haddock. -HADDOCK ?= haddock - -# URL prefix leading to Haddock documentation for the hierarchical -# libraries. -GHC_DOC_URL ?= http://www.haskell.org/ghc/docs/latest/html/libraries - -# Path prefix leading to Haddock interface files for the hierarchical -# libraries. These files should be compiled using a Haddock program -# which is interface compatible with the one listed above (same -# version). -GHC_DOC_PATH ?= /usr/local/share/doc/ghc/libraries/ - -# Documentation is stored in this directory. Note that the directory -# is emptied first. -DOCDIR = docs - hunk ./Makefile 16 -# PKGS is PACKAGES but without the numeric suffices. Unfortunately -# PKGS=$(foreach pkg,$(PACKAGES),`echo $(pkg) | sed -r -e 's/-.*//'`) -# does not quite work, so I have resorted to the following ugly hack: - -PKGS=$(basename $(basename $(basename $(basename $(subst -,.,$(PACKAGES)))))) - -EXPOSED_SOURCES = ChasingBottoms.hs ChasingBottoms/Approx.hs \ -ChasingBottoms/ApproxShow.hs ChasingBottoms/ContinuousFunctions.hs \ -ChasingBottoms/IsBottom.hs ChasingBottoms/Nat.hs \ -ChasingBottoms/SemanticOrd.hs ChasingBottoms/TimeOut.hs - -HIDDEN_SOURCES = ChasingBottoms/IsType.hs ChasingBottoms/Tests.hs \ -ChasingBottoms/Approx/Tests.hs ChasingBottoms/ApproxShow/Tests.hs \ -ChasingBottoms/ContinuousFunctions/Tests.hs \ -ChasingBottoms/IsBottom/Tests.hs ChasingBottoms/IsType/Tests.hs \ -ChasingBottoms/Nat/Tests.hs ChasingBottoms/SemanticOrd/Tests.hs \ -ChasingBottoms/TimeOut/Tests.hs ChasingBottoms/TestUtilities.hs \ -ChasingBottoms/TestUtilities/Generators.hs \ -ChasingBottoms/TestLibraryWhenCompiling.hs - -FILES_TO_BE_EXCLUDED = .boring - -$(DOCDIR) : $(DOCDIR)/index.html -$(DOCDIR)/index.html : $(addprefix Test/,$(EXPOSED_SOURCES)) Header - -rm -rf $(DOCDIR) - mkdir -p $(DOCDIR) - $(HADDOCK) -h --title="Chasing Bottoms" --prologue=Header -o$(DOCDIR) \ - $(foreach pkg,$(PKGS),\ - -i$(GHC_DOC_URL)/$(pkg),$(GHC_DOC_PATH)/$(pkg)/$(pkg).haddock) \ - $(filter Test/%,$^) - -# Target used by darcs dist. -# After building the documentation we remove the generated files. We -# do not want them included in the tar ball generated by darcs. -# We also remove some other files. -dist: $(DOCDIR) - -rm $(FILES_TO_BE_EXCLUDED) - changepref predist make dist }