[Haskell-cafe] property testing with context
olf at aatal-apotheke.de
Fri Oct 19 20:53:38 UTC 2018
the solution might be simple: Don't express the property as an atomic function (a -> Bool).
This reminds me a bit of the Cutty-Howard correspondence, only that proofs are replaced by counterexamples. A testing library should have an operator for each of the logical connectives, where
- a counterexample to True is never found
- a counterexample to False is ()
- a counterexample to (not x) is an example for x
- a counterexample to (x && y) is either a counterexample to x or a counterexample to y, whichever is found first
- a counterexample to (x || y) is a pair of counterexamples to both x and y
- a counterexample to (x ==> y) is an example for x together with a counterexample for y
Then, if you build your property out of smaller properties and the connectives above, the counterexample-finder would be able to inform you which part of the property failed. I'm pretty sure at least one of the testing libraries has a system like this.
More information about the Haskell-Cafe