4 ms·
A fun riff on QuickCheck is QuickSpec[1], a tool that automatically generates laws (invariants) for an API and tests them with QuickCheck. The example in the do
by tikhonj 10y ago
A fun riff on QuickCheck is QuickSpec[1], a tool that automatically generates laws (invariants) for an API and tests them with QuickCheck. The example in the documentation is pretty good:
Given reverse, ++ (list concatenation) and [], it finds six laws:
xs ++ [] == xs
[] ++ xs == xs
(xs ++ ys) ++ zs == xs ++ (ys ++ zs)
reverse [] == []
reverse (reverse xs) == xs
reverse xs ++ reverse ys == reverse (ys ++ xs)
It's not perfect—it's limited to reasonably small equational laws on a small set of provided functions—but I think it's a really cool example of what's possible and even practical starting from a simple and elegant tool like QuickCheck.
[1]: https://hackage.haskell.org/package/quickspec https://hackage.haskell.org/package/quickspec
- ZenoArrow 10y agoI've been looking for a tool like QuickSpec, thank you for mentioning it.
- nickpsecurity 10y agoAnd, per mbrock, you can feed that into HipSpec: http://www.cse.chalmers.se/~jomoa/papers/hipspec-atx.pdf http://www.cse.chalmers.se/~jomoa/papers/hipspec-atx.pdf https://github.com/danr/hipspec https://github.com/danr/hipspec
- taeric 10y agoIf only my bugs were as simple as the methods reverse, concat, and index... Granted, to an extent, my bugs probably were as simple as that. But it was as likely an emergent simplicity. Not to mention that one of my laws will be performance. This is like showing how awesome a language is with a to-do app. Neat. Possibly educational. Mostly an exercise in how well the author knew how to write a to-do app.
- mbrock 10y agoIf only your core logic had some straightforward invariants... QuickCheck can work effectively with complex data structures. For an example of a simple invariant that can still uncover subtle and important bugs: encode(decode(X)) = X Where encode and decode are some domain specific blobs of protocol logic. It's pretty useful to have the computer verify that isomorphism with a huge number of generated inputs. (There's also SmallCheck which is like QuickCheck but checking all possible values within some depth limit, instead of random values.) And there's no reason you couldn't use QuickCheck to verify a performance law, by the way.
- dllthomas 10y ago> And there's no reason you couldn't use QuickCheck to verify a performance law, by the way. In fact, I've done something similar to this.
- taeric 10y agoI'd be interested in seeing how you did this.
- dllthomas 10y agoMore precisely what I did was minimization on an unusually slow example input, but I don't think I can share the code. The approach generalizes, though: To verify performance, you would set it up to benchmark the code in question (in Haskell, this would probably mean using Criterion) and then assert that it was "fast enough" (probably relative to the size of the input).
- taeric 10y agoMy complaint was less against quick check, and more against the examples. Pedagogically themed ideas make sense. Practical and visible results are better. By orders of magnitude.
- mavelikara 10y ago> If only my bugs were as simple as the methods reverse, concat, and index... When I first read about QuickCheck, I had similar reaction. But then I learned that QuickCheck can test stateful systems also. For example, this bug reported against LevelDB, a database system developed at Google, was discovered using QuickCheck: https://github.com/google/leveldb/issues/50 https://github.com/google/leveldb/issues/50. You can read more about it at http://htmlpreview.github.io/?https://raw.github.com/strangeloop/lambdajam2013/master/slides/Norton-QuickCheck.html http://htmlpreview.github.io/?https://raw.github.com/strange...
- taeric 10y agoThese links are awesome. More examples of real world successes go a long way to not just impressing with technical ability, but convincing of practical use. That is quick check impresses me. I just haven't seen many real world examples of it providing significant value. And I no longer buy in to appealing arguments. :(
- querulous 10y agothis might be of interest: https://medium.com/@jlouis666/breaking-erlang-maps-1-31952b8729e6#.90i0j6asc https://medium.com/@jlouis666/breaking-erlang-maps-1-31952b8...