Most posts about property-based testing focus on convincing the reader to do property-based tests and the mechanics of writing the tests.
Unfortunately, I'm already convinced and know how to write the tests — what I wish I could find is some resource that would hone my ability to identify worthwhile properties. The best one I know of and go back to time and time again is https://fsharpforfunandprofit.com/posts/property-based-testi..., but I really wish I could find more.
I really liked Hebert's Property-Based Testing with PropEr, Erlang, and Elixir. It's in Erlang and Elixir, but the concepts transfer well to other languages and property-based test systems.
Thanks! This page is familiar so I've definitely read it before, but didn't recall it when remembering examples. I like that it links to the site I provided; maybe I should try to search for other articles that also link there to find more inspiration.
I've had a good experience with this[0], however it seems Eric is not currently running it, if you're interested, email me, I can dig around and see if I can find my notes.
Alternatively reach out to him in an email and see if he'll be willing to let you buy access. I personally found it a pretty good course where he had spent a reasonable amount of time coming up with both decent examples to highlight how it was going to work as well as create some nice rules of thumb as starting points to think about properties.
Explore abstract algebra[0]. It’s the study of algebraic structures, which are sets (types/classes) and operators (functions/methods) with axioms (properties). Also check out binary relations[1], part of order theory.
It looks like Arbitrary will sample integers from an uniform distribution. For property based testing you often would like to have a bias towards "interesting" values that might trigger special cases, like -1, 0 and 1.
E.g. if you had "max_speed_kph: Option<u64>", your tests might never check what happens if max_speed_kph is 0.
One also may bias values to be similar (or equal) to other recently generated values. This was a trick used in the compiler tester yarpgen, where it was useful in testing optimization of bitwise operators on integers.
There are a couple of useful things missing here at a glance. One is shrinking, where the library will attempt to find simpler cases of failures rather than just brute force a random one. Second is how to create related pieces of data that are constrained in some way, above and beyond pure random bytes, but I assume there’s some way here to manually interpret the random bytes. But sometimes you have to hand-tune these things because you don’t just want to wait for the RNG to guess the right combination to create valid data.
I’ve had some success with property based testing, at least for heavily algorithmic code. For example I wrote a kNN implementation after finding all sorts of edge cases in others (floating point shenanigans included). You can succinctly capture properties like: returning the right number of clusters, each point being closest to its cluster’s mean, each cluster being centred on its centroid, all points being assigned to a cluster, and all clusters being non-empty. But even then you could game things if you wanted to.
Where I’ve struggled is in the general case. Most tests don’t have good property based alternatives, beyond just repeating the logic of the code under test, which seems pointless. And so you have this constant tension of wondering if a particular test could or should be property based.
The value in property based tests is that the original libraries (Quickchwck, both Haskell and Erlang) try to find the smallest reproducible error sample, and then display that sample to you.
And that (Quickcheck at least) has a bunch of primitive generators that you build your structures out of.
No idea, if it's doable in Rust. I just find it strange that it works on a stream of random bytes out of which you magically get some structures.
Meta question: do many people use property-based testing in their production systems? I think the philosophical idea is extremely sound and is a very good approximation to proving correctness, but I only ever see trivial examples like "a + b = b + a" as a property. How does property-based testing hold up in far larger systems with quite complex setup behaviors?
If you enjoy reading Rust code, you can see some examples I have...
1. This example [1] compares a SIMD-accelerated implementation of an algorithm vs the naive implementation. This is usually referred to as an "oracle".
2. This example [2] tests an XML document object model library. The tests construct a sequence of operations to apply to a document ("add an element", "delete an element", "move an element" etc) and then assert properties that you expect to be true for a DOM tree (a parent and child are always cross-linked, for example)
I have used it in multiple production systems, even fairly complicated ML-based ones. But also to verify integrity of low-level components that have complex performance optimisations. It has only been met with positive feedback, of the "what a clever way to generate test cases" kind.
The difficult bit is finding invariants or approximations, but doing so is half of what makes the code more robust anyway!
The operational problem is that the tests sometimes take a little longer to run, so sometimes they have to be in a low-prio suite.
Property based testing is quite common for compilers, I think. Generate valid programs, then see if the compiled code does the same thing on different settings (or versus a different compile.) Or, modify the program in a way that should preserve the meaning and see if the compiled code does the same thing.
Fuzzing can be thought of as property based testing.
The key to PBT is that it allows tests to be generated and minimized automatically, enabling enormously larger volumes of tests than if the tests have to be generated manually.
I am far from being an expert in the field, but I have seen property based tests used to verify complex stateful systems.
I remember more circa 2010 attending a presentation by the guys from QuviQ who mentioned that their solution was used by the automotive industry in Sweden to verify embedded systems.
Our biggest use case has been testing our database materialization. We have a somewhat complicated hierarchical organization tree/forest within our database. In order to efficiently query those structures, we materialize the transitive closure of these relationships. TL;DR; we populate a row for each (org, ancestor) and maintain that via postgres triggers that fire whenever we mutate things.
The prop test that tests it all does three things. First, it establishes an arbitrary that captures all the possible shapes of organization trees. Second, we define the set of mutations (add a child, switch parents, delete a grandparent, etc.) that may occur. Third, we have code for reading/writing org trees to and from the DB.
The test then generates an org tree, syncs it to the db, performs 1 or more mutations on the tree and then compares what's in the database with the resulting tree.
Overall it's been pretty great. I highly recommend property tests, especially when modeling complex data in an external system.
I've done a similar thing myself when trying to test operations on a hierarchical database for my internal product.
Biggest difficulty for me was that some combinations of operations were illegal and I had to think about all the edge cases and filter them out, and this took a long time.
My SO works in hardware, and she says they always use a constraint solver to generate test cases / test vectors, and she never understood why this wasn't popular in software. I googled it a bit and found lots of academic papers but no concrete implementation.
I've also thought about generating test vectors using a generator based on Markov chains, I wrote about that here [0], based on this [1] submission.
I'm not familiar enough with either using constraint solvers to generate test cases, or Markov chains, to know if I'm talking nonsense here or is it just something that nobody thought to develop properly.
I had a really hard time getting past the bad construction of the struct. Why not make an enum variant where a bike just doesn't have a fuel property. Makes things a lot easier.
Unfortunately, I'm already convinced and know how to write the tests — what I wish I could find is some resource that would hone my ability to identify worthwhile properties. The best one I know of and go back to time and time again is https://fsharpforfunandprofit.com/posts/property-based-testi..., but I really wish I could find more.