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