[Haskell-cafe] property testing with context

[Oliver Charles]

Perhaps the work in my "assert-explainer" project is relevant here -
https://github.com/ocharles/assert-explainer.

The idea is your tests should just be writing "assert
someArbitraryExpressionEvaluatingToBool", and then having some
compiler magic recover the context for you when it goes wrong. To cite
my own README:


You write:

    assert (length xs == 4)

No need for lots of special assertEqual etc functions.

When the assertion fails, you will get much more context:

✘ Assertion failed!
    length xs == 4 /= True (at Test.hs:18:12-25)

  I found the following sub-expressions:
    - length xs = 3
    - xs = [1,2,3]


This is done via a GHC source plugin that rewrites "assert (length xs
== 4)" into an expression that - if False - prints much more
information.

It's very early days for this plugin, but the goal is to reach parity
with https://docs.pytest.org/en/latest/example/reportingdemo.html#tbreportdemo.

Hope this helps,
Ollie
On Fri, Oct 19, 2018 at 8:20 AM Ben Franksen <ben.franksen at online.de> 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?
>
> 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.