QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs (2000) [pdf]
cs.tufts.edu
cs.tufts.edu
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)
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.
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.
In fact, I've done something similar to this.
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).
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. You can read more about it at http://htmlpreview.github.io/?https://raw.github.com/strange...
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. :(
(disclosure: I have some pretty large Erlang QuickCheck models on Github)
I think my first introduction to property based testing was this video [1] from F# for fun and profit. The speaker does a great job at presenting the topic in a way that's clear and approachable. Ff you prefer text over video, on the same post there's links to other blog posts which cover the same material.
I've just discovered generative testing due to clojure.spec. Describing specs for your data works not only to help validate data structures but can be plugged in as properties for generative testing.
After the "aha" moment it was followed by a feeling that I've wasted so much time writing specs just to validate data structures and writing specs just to see if my functions are working as they should.
This is one of the things I wish was obvious in my learning track right after vim/emacs will help you code faster.
(As I said, it was a skim - I'd love to be wrong!)
I have a function takes a list and fails if it has more than two negative numbers in.
Quickcheck first finds a failing test with a list of 200 numbers in. It then tries removing parts of the list to see if it can find a smaller failing example. The final output ends up (hopefully) as [-1,-1,-1]
Much easier to debug than a 200 element input.
I found this very useful when creating a tester for guis because I'd get minimal ui examples where things failed.
Minimization is the process of starting from that known value and simplifying it as much as possible while still failing the test. For example QuickCheck discovers a 1235 element list, that fails. The problem happens to be a 0 in the last element. Minimisation might simplify that list to [1, 0]. So finding the cause is quite a bit easier.
To be fair though, QuickCheck is not completely random. It has a "size" parameter that starts small and grows, thus allowing small values to be tested first.
Because you want to test things in the order that will most quickly find you a small error. This winds up being a trade-off, and as you say QuickCheck doesn't start with arbitrarily large inputs. But just testing all small inputs in order is often not the best choice.
For example, if your function takes an unsigned 32 bit integer, and you've tested inputs 0 through 15161, do you expect you're more likely to find an error next testing 15162, or 4294967295?