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.
