[prev in list] [next in list] [prev in thread] [next in thread]
List: haskell-cafe
Subject: Re: [Haskell-cafe] property testing with context
From: Oliver Charles <ollie () ocharles ! org ! uk>
Date: 2018-10-24 20:51:31
Message-ID: CAGRp5RnPRggac19doPjJSye4ZpQDsx=bWENC_5-Mbak+9xLE1w () mail ! gmail ! com
[Download RAW message or body]
[Attachment #2 (multipart/alternative)]
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.
On Wed, 24 Oct 2018, 2:44 pm , <amindfv@gmail.com> wrote:
> 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@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.
> _______________________________________________
> 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.
[Attachment #5 (text/html)]
<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>
[Attachment #6 (text/plain)]
_______________________________________________
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.
[prev in list] [next in list] [prev in thread] [next in thread]
Configure |
About |
News |
Add a list |
Sponsored by KoreLogic