[Haskell-cafe] property testing with context
amindfv at gmail.com
amindfv at gmail.com
Wed Oct 24 13:44:23 UTC 2018
Agreed, I think QuickCheck is already up to the task. The simpler prop_recommute could be rewritten with (===), (.&&.), and maybe "counterexample" to label which branch failed.
Tom
> El 22 oct 2018, a las 05:59, arjenvanweelden at gmail.com escribiÃ³:
>
>> On Fri, 2018-10-19 at 09:19 +0200, Ben Franksen wrote:
>> Hi everyone
>>
>> it seems to be the season for new variations on the "property
>> testing"
>> theme, so I would like to chime in... not to announce a new library,
>> sadly, but with a rough idea how the existing ones could perhaps be
>> improved, based on practical experience in Darcs.
>>
>> The problem I have is that there is a tension between
>>
>> (a) stating a property in a clear and simple way, so its code doubles
>> as
>> a formal specification
>>
>> and
>>
>> (b) writing the property in such a way that when it fails, the
>> reported
>> value(s) give enough information about the context to be useful for
>> finding the cause of the problem.
>>
>> Let me give an example to demonstrate what I mean.
>>
>> There is a simple law that says if a sequential pair of patches A;B
>> commutes to B';A' then B';A' commutes back to A;B. In code this looks
>> (more or less) like this:
>>
>> prop_recommute :: Commute p => (p :> p) wA wB -> Bool
>> prop_recommute (x:>y)
>> | Just (y':>x') <- commute (x:>y) =
>> case commute (y':>x')of
>> Just (x'':>y'') -> x==x'' && y==y''
>> Nothing -> False
>> | otherwise = True
>>
>> This is a bit more verbose than the informal spec but still quite
>> readable.
>>
>> Now suppose this property fails. So quickcheck reports the counter
>> example pair (X:>Y) for some X and Y. But that isn't too useful in
>> itself. We'd like to know a bit more:
>>
>> * did the second commute fail?
>> * or did it succeed but x/=x'' or y/=y''?
>> * and in the latter case, which of the two?
>
> I think that this is possible by simply using QuickCheck's === and ==>
> (if you have Show and Eq instances for :>):
>
> prop_recommute :: Commute p => (p :> p) wA wB -> Bool
> prop_recommute (x:>y)
> = isJust commuted ==> commute commuted === Just (x:>y)
> where
> commuted = commute (x:>y)
>
> See
> https://hackage.haskell.org/package/QuickCheck-2.11.3/docs/Test-QuickCheck-Property.html
> for information on ==> and ===.
>
> This is more readable and quite similar to your example above. It would
> print both left and right side of === when a counter-example is found.
>
> Depending on your implementation of Show for :>, it could look
> like: Nothing /= Just (...A... :> ...B...) or Just (...A... :> ...B...)
> /= Just (...C... :> ...D...).
>
> I did not try this myself, so I could have made a mistake or I may have
> missed why this is not good enough for your case.
>
>> So in practice our property code looks more like this:
>>
>> prop_recommute :: (ShowPatch p, Commute p) => (p :> p) wA wB -> Bool
>> prop_recommute (x :> y)
>> | Just (y' :> x') <- commute (x :> y) =
>> case commute (y' :> x') of
>> Nothing ->
>> failed (redText "failed, where x" $$ displayPatch x $$
>> redText ":> y" $$ displayPatch y $$
>> redText "y'" $$ displayPatch y' $$
>> redText ":> x'" $$ displayPatch x')
>> Just (x'' :> y'') ->
>> if y'' /= y
>> then
>> failed (redText "y'' =/\\= y failed, where x" $$
>> displayPatch x $$
>> redText ":> y" $$ displayPatch y $$
>> redText "y'" $$ displayPatch y' $$
>> redText ":> x'" $$ displayPatch x' $$
>> redText "x''" $$ displayPatch x'' $$
>> redText ":> y''" $$ displayPatch y'')
>> else
>> if x'' /= x
>> then
>> failed (redText "x'' /= x, where x" $$
>> displayPatch x $$
>> redText ":> y" $$ displayPatch y $$
>> redText "y'" $$ displayPatch y' $$
>> redText ":> x'" $$ displayPatch x' $$
>> redText "x''" $$ displayPatch x'' $$
>> redText ":> y''" $$ displayPatch y'')
>> else True
>> | otherwise = True
>>
>> Now this code tells us exactly what went wrong when the property
>> fails
>> but it is ugly and repetitive and the additional code obscures the
>> simple logical content. So this is no longer quite as suitable for a
>> (human readable) formal spec.
>>
>> I wonder if displaying
>>
>> (1) all relevant contextual variables and
>> (2) "where in the code it fails"
>>
>> could be automated away, somehow. I guess this is not trivial and may
>> require syntactic analysis, so perhaps expecting a /library/ to solve
>> the problem is unrealistic, except perhaps by using Template Haskell.
>> I'd also go with a separate tool that extracts properties from a
>> module
>> and enriches them with code that displays the additional information.
>>
>> Tackling this problem might be an interesting theme for a master
>> thesis... ;-)
>>
>> Cheers
>> Ben
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> To (un)subscribe, modify options or view archives go to:
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>> Only members subscribed via the mailman list are allowed to post.
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
More information about the Haskell-Cafe
mailing list