There is the forAll quantifier that returns a property which checks if all test cases pass. Is there a way to define a "there exists" quantifier that returns a property which checks it at least one test case passes?
Testing existence by enumeration would be more reliable: SmallCheck, LeanCheck, FEAT.
If you must use random generation there are some indirect ways in QuickCheck.
expectFailure seems like a good candidate for negation. However it isn't quite it, as it isn't involutive so you must negate the property in other ways, like not, if your property is in fact boolean.
exists :: Gen a -> (a -> Bool) -> Property
exists gen prop = once $ expectFailure (forAll gen (not . prop))
This counts crashing as a failure though, which thus makes the test pass even though you might not expect it.
Existential quantification is kind of a disjunction, and QuickCheck has disjoin. Just make a huge enough disjunction.
exists :: Gen a -> (a -> Property) -> Property
exists gen prop = once $ disjoin $ replicate 10000 $ forAll gen prop
But you get spammed with counterexamples when no good example is found.
Maybe it is better to rewrite the logic of forAll yourself to avoid the call to counterexample.
More simply you can always write your own property as a generator to get the proper quantification.
exists :: Gen a -> (a -> Bool) -> Property
exists gen prop = property (exists' 1000 gen prop)
exists' :: Int -> Gen a -> (a -> Bool) -> Gen Bool
exists' 0 _ _ = return False
exists' n gen prop = do
a <- gen
if prop a
then return True
else exists' (n - 1) gen prop
Doing this manually also has the property that if prop unexpectedly crashes, it is immediately reported as a failure, as opposed to the previous methods.
EDIT
So if you only have a (a -> Property) instead of (a -> Bool) it seems much trickier to achieve a good result, because it's non-trivial to check whether a property succeeded. A proper way would be to mess with the internals of QuickCheck, probably something similar to disjoin. Here is a quick hack
Use
mapResultto silence the output ofdisjoinwhen no (counter)example was found.Override the size parameter because if your witnesses are non-trivial, they will not be found if the size is too small or too large.
import Test.QuickCheck
import Test.QuickCheck.Property as P
-- Retry n times.
exists :: Testable prop => Int -> Gen a -> (a -> prop) -> Property
exists n gen prop =
mapResult (\r -> r {P.reason = "No witness found.", P.callbacks = []}) $
once $
disjoin $
replicate n $ do
a <- gen
return (prop a)
main = quickCheck $ exists 100
(resize 5 arbitrary)
(\x -> (x :: Integer) == 2)
-
Your third suggestion is close to what I'm looking for. But in order to combine it with
forAll, for example to writeexists gen1 $ \a -> forAll gen2 ..., exists would have to have signature(Testable prop) => Gen a -> (a -> prop) -> Property. I've trouble finding out how to do this reading QuickCheck's source code. Would you know how to do it? – Guillaume Chérel Mar 15 '17 at 14:19 -
I guess my example relies a lot on the property being simply boolean. If you have an abstract
propyou can use.||.ordisjoin, which ends up resembling what I suggested in the second example about not callingcounterexample. – Li-yao Xia Mar 16 '17 at 12:30 -
1
once $ disjoin $ replicate 10000 $ do { a <- gen ; return (prop a) }But as I said, it silences exceptions. It turns out you can usemapResultas suggested by Alexey Romanov to check for exceptions raised at the end ofdisjoin. – Li-yao Xia Mar 16 '17 at 12:36 -
Your last suggestion seems to work but takes a long time and fills the console with empty lines. I've spent days on it but I still can't figure out how to do this properly. Could you rewrite your 3rd suggestion in your post so that it works with a Testable prop instead of a Bool? The whole problem I can't solve is how to check if
prop ais a success of a failure. – Guillaume Chérel Mar 22 '17 at 17:33 -
I appended something that seems to work, still with
disjoin. Unfortunately I couldn't figure out a good way based on a pure generator (mainly because I'm not familiar enough with the internals ofProperty). Somehowoncedoesn't have the effect I expected. Sorry if that answer is still unsatisfactory. – Li-yao Xia Mar 22 '17 at 22:42
I don't know if something like this exist in QuickCheck. Also not convinced it would be helpful, but that's another matter. Since we have:
∃ x . P x <=> ¬ ¬ ∃ x . P x <=> ¬ ∀ x . ¬ P x
I suppose you could set it up so your test-case tests the negation and if it fails it means you have your existential. HTH.
-
-
I've thought about that, but how do you take the negation of
forAll ...in quickCheck? I've already triednot (forAll gen prop)butforAllreturns a Property antnotexpects a Bool. – Guillaume Chérel Mar 13 '17 at 13:43 -
1@GuillaumeChérel You should be able to implement it using
mapResult: hackage.haskell.org/package/QuickCheck-2.9.2/docs/src/…. – Alexey Romanov Mar 13 '17 at 14:25
length a < 0. So the length should be less than0. It is clear it will never be satisfied. So the tests will get stuck into an infinite loop where they will keep generating lists in the hope one of them will have a lenght less than0. Now you cannot make a distinction between: "not satisfied because the condition is rare", or "unsatisifiable". – Willem Van Onsem Mar 13 '17 at 13:35forAllanyway: you cannot make a distinction between "satisfied because the counter example is rare" and "true". – Guillaume Chérel Mar 13 '17 at 13:50