[Haskell-cafe] property testing with context

[amindfv at gmail.com]

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.