[Haskell-cafe] property testing with context

[arjenvanweelden at gmail.com]

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.