[Haskell-cafe] property testing with context

[Olaf Klinke]

Ben,

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. 

Cheers,
Olaf