There's a fun property-testing library for Haskell called LazySmallcheck (and a more powerful version called LazySmallcheck2012) which is sort-of coverage-based. Since Haskell values are lazy, it uses exceptions as its test data: if a particular exception gets thrown, the test must have forced that part of the test data, so it replaces that part and tries again.
For example, let's say our test data is an assoc-list like `[(Int, Customer)]`, and there's a bug that's triggered by repeated keys. LazySmallcheck will run the test on the most general assoc-list there is, a _|_ value!
myTest (exception A) --> throws A
Since A was thrown, LSC will try again; making the list slightly more specific; which means trying both constructors `[]` and `:`:
myTest [] --> test passes
myTest (exception A:exception B) --> throws A
The input `[]` is completely specified, and it didn't lead to any counterexample, so LSC is finished with that branch. In the `:` branch, the general pair `exception A` caused an error, so LSC will make it slightly more specific and try again:
myTest ((exception A, exception C):exception B) --> throws A
Since `exception A` is an Int, LSC can't use laziness to keep things general; it has to try concrete values, so it proceeds like Smallcheck; trying the "smallest" Int values:
myTest ((0, exception C):exception B) --> throws B
Again, LSC will make the general list `exception B` more specific:
myTest ((0, exception C):[]) --> passes
myTest ((0, exception C):exception A:exception B) --> throws A
Since the input `(0, exception C):[]` passed the test without triggering the exception, we know the second element of that pair must be irrelevant to the result. In other words, LSC has proved the property holds for inputs `(0, X):[]` for all X!
LSC hence won't try specialising `exception C`; but it will try "larger" Int values, e.g. `(1, exception C):[]`, `(-1, exception C):[]`, etc. up to a pre-defined "depth". I'll ignore these cases and focus on the branch with the longer list:
myTest ((0, exception C):(exception A, exception D):exception B --> throws A
Again, LSC will specialise the general Int `exception A` into specific values, starting with the "smallest":
myTest ((0, exception C):(0, exception D):exception B) --> FAIL!
This input has duplicate keys, which triggered the bug and caused our test to fail. Again, the fact that the exceptions inside this value didn't get thrown means those parts were irrelevant to the result. LSC indicates irrelevant values with `_`, so it will report this counterexample as `(0, _):(0, _):_`.
That's more informative for understanding this bug than e.g. Smallcheck or QuickCheck, whose "minimal" counterexamples would be fully-specified values, like `(0, Customer { name = "", orders = [], discount = Nothing, joined = 1970-01-01 }):(0, Customer { name = "", orders = [], discount = Nothing, joined = 1970-01-01 }):[]`.
Hence LSC's approach has three interesting features:
- It has a coverage-like approach that homes-in on interesting cases, by gradually generating the parts of a value that get forced (which are usually the parts being branched on)
- It can indicate which parts of a counterexample are irrelevant for the failure
- It can prove some properties universally (i.e. when that input is irrelevant to the pass result)
For example, let's say our test data is an assoc-list like `[(Int, Customer)]`, and there's a bug that's triggered by repeated keys. LazySmallcheck will run the test on the most general assoc-list there is, a _|_ value!
Since A was thrown, LSC will try again; making the list slightly more specific; which means trying both constructors `[]` and `:`: The input `[]` is completely specified, and it didn't lead to any counterexample, so LSC is finished with that branch. In the `:` branch, the general pair `exception A` caused an error, so LSC will make it slightly more specific and try again: Since `exception A` is an Int, LSC can't use laziness to keep things general; it has to try concrete values, so it proceeds like Smallcheck; trying the "smallest" Int values: Again, LSC will make the general list `exception B` more specific: Since the input `(0, exception C):[]` passed the test without triggering the exception, we know the second element of that pair must be irrelevant to the result. In other words, LSC has proved the property holds for inputs `(0, X):[]` for all X!LSC hence won't try specialising `exception C`; but it will try "larger" Int values, e.g. `(1, exception C):[]`, `(-1, exception C):[]`, etc. up to a pre-defined "depth". I'll ignore these cases and focus on the branch with the longer list:
Again, LSC will specialise the general Int `exception A` into specific values, starting with the "smallest": This input has duplicate keys, which triggered the bug and caused our test to fail. Again, the fact that the exceptions inside this value didn't get thrown means those parts were irrelevant to the result. LSC indicates irrelevant values with `_`, so it will report this counterexample as `(0, _):(0, _):_`.That's more informative for understanding this bug than e.g. Smallcheck or QuickCheck, whose "minimal" counterexamples would be fully-specified values, like `(0, Customer { name = "", orders = [], discount = Nothing, joined = 1970-01-01 }):(0, Customer { name = "", orders = [], discount = Nothing, joined = 1970-01-01 }):[]`.
Hence LSC's approach has three interesting features:
- It has a coverage-like approach that homes-in on interesting cases, by gradually generating the parts of a value that get forced (which are usually the parts being branched on)
- It can indicate which parts of a counterexample are irrelevant for the failure
- It can prove some properties universally (i.e. when that input is irrelevant to the pass result)