lazy-smallcheck-2012

Last updated: 2020-01-08 11:59:03 +0000

Upstream URL: git clone http://chriswarbo.net/git/lazy-smallcheck-2012.git

Repo

View repository

View issue tracker

Contents of README.md follows


LazySmallCheck2012

Lazy SmallCheck with functional values and existentials!

Build Status

<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.

Motivation

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 <code>foldr</code>.

<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">prop_ReduceFold ::</span> ([<span class="dt">Bool</span>] <span class="ot">-></span> <span class="dt">Bool</span>) <span class="ot">-></span> <span class="dt">Property</span> prop_ReduceFold r <span class="fu">=</span> existsDeeperBy (<span class="fu">+</span><span class="dv">2</span>) <span class="fu">$</span> \f z <span class="ot">-></span> forAll <span class="fu">$</span> \xs <span class="ot">-></span> r xs <span class="fu">==</span> foldr f z xs</code></pre></div>

When this property is tested using our advanced version of <em>Lazy SmallCheck</em>, a small counterexample is found for <code>r</code>.

<pre><code>>>> test prop_ReduceFold ... LSC: Depth 2: LSC: Counterexample found after 374 tests. Var 0: { [] -> False ; _:[] -> False ; _:_:_ -> True } *** Exception: ExitFailure 1 </code></pre>

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, <code>r</code> and <code>f</code>, 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 <code>r</code> is <em>concise</em> and easy to understand.

The previous version of Lazy SmallCheck did not include any of these features.

Usage

<em>Note: Follow this until I upload it to Hackage.</em>

<ol style="list-style-type: decimal"> <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" style="list-style-type: decimal"> <li>

Try some simple properties over <code>Prelude</code> 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.

<pre><code>*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></code></pre>