[Haskell-cafe] property testing with context
Oliver Charles
ollie at ocharles.org.uk
Wed Oct 24 20:51:31 UTC 2018
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 at 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 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.
> _______________________________________________
> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20181024/f9a94d2c/attachment.html>
More information about the Haskell-Cafe
mailing list