Last updated: 2024-01-19 11:17:17 +0000
Upstream URL: git clone http://chriswarbo.net/git/lazy-smallcheck-2012.git
Contents of README.md follows
Lazy SmallCheck with functional values and existentials!
<em>This code is mid-clean up. Many features are not yet included. Watch this space.</em>
A property-based testing library enables users to perform lightweight verification of software. This repo presents improvements to the Lazy SmallCheck property-based testing library. Users can now test properties that quantify over first-order functional values and nest universal and existential quantifiers in properties. When a property fails, Lazy SmallCheck now accurately expresses the partiality of the counterexample. The necessary architectural changes to Lazy SmallCheck result in a performance speed-up. All of these improvements are demonstrated through several practical examples.
Consider the following conjectured property that in Haskell all
reductions on lists of Boolean values to a single Boolean value can be
expressed as a foldr
.
prop_ReduceFold :: ([Bool] -> Bool) -> Property
prop_ReduceFold r = existsDeeperBy (+2) $ \f z -> forAll $ \xs -> r xs == foldr f z xs
When this property is tested using our advanced version of <em>Lazy
SmallCheck</em>, a small counterexample is found for r
.
>>> test prop_ReduceFold
...
LSC: Depth 2:
LSC: Counterexample found after 374 tests.
Var 0: { [] -> False
; _:[] -> False
; _:_:_ -> True }
*** Exception: ExitFailure 1
Reading the output in the style of Haskell’s case-expression syntax
in explicit layout, this function tests for a multi-item list. Several
new features of Lazy SmallCheck are demonstrated by this example. First,
note that two of the quantified variables, r
and
f
, are <em>functional values</em>. Secondly, an
<em>existential quantifier</em> is used in the property definition.
Thirdly, the property involves <em>nesting of universal and existential
quantifiers</em> inside the property. Finally, the counterexample found
for r
is <em>concise</em> and easy to understand.
The previous version of Lazy SmallCheck did not include any of these features.
<em>Note: Follow this until I upload it to Hackage.</em>
<ol type="1"> <li>Download this repository.
$ git clone https://github.com/UoYCS-plasma/LazySmallCheck2012.git $ cd LazySmallCheck2012 $ cabal install –only-dependencies
</li> <li>Enter the GHC interactive mode.
$ ghci … ########################################## # LazySmallCheck 2012 GHCi Environment # ########################################## :suite — Run test suite. :lsc2012 — Reset environment. :readme — View README.md.
*LSC2012>
</li> <li>Run the test suite to ensure that everything is working correctly. If it doesn’t, please report the issue.
*LSC2012> :suite … Suite: Test suite complete.
Press <ENTER> to continue…
</li> </ol>Hit enter to continue and you’ll return to the environment from (3).
<ol start="5" type="1"> <li>Try some simple properties over Prelude
types. For
example;
*LSC2012> test $ xs -> head (x : (xs :: [Int])) == x LSC: Depth 0: LSC: Property holds after 1 tests. LSC: Depth 1: LSC: Property holds after 4 tests. LSC: Depth 2: LSC: Property holds after 6 tests. … LSC: Depth 137: LSC: Property holds after 276 tests. <CTRL-C>
</li> </ol>Or a failing property.
*LSC2012> test $ \xs n -> length (take n (xs :: [Int])) == n
LSC: Depth 0:
LSC: Property holds after 1 tests.
LSC: Depth 1:
LSC: Counterexample found after 2 tests.
Var 0: _
Var 1: -1
*** Exception: ExitFailure 1
*LSC2012> test $ \xs n -> 0 <= n ==> length (take n (xs :: [Int])) == n
LSC: Depth 0:
LSC: Property holds after 1 tests.
LSC: Depth 1:
LSC: Counterexample found after 5 tests.
Var 0: []
Var 1: 1
*** Exception: ExitFailure 1
*LSC2012> test $ \xs n -> 0 <= n ==> length (take n (xs :: [Int])) <= n
...
<CTRL-C>