A real-world case of property-based verification

I love seeing real-world examples of testable properties :) It's hard, when starting out with property testing, to think of good properties off the top of your head. Sometimes you can generalize from a unit test of one case to a "for all x" case, but the real world is often much messier. Still, some that often show up, and are easily testable:

• idempotency, sort(x) == sort(sort(x))
• inverses/round-tripping, encode(decode(x)) == x
• symmetry, union(a,b) == union(b,a)
• associativity, concat(concat(xs, ys), zs) == concat(xs, concat(ys, zs))
• "zero elements", lst == concat(lst, emptylist)
• monotonicity, length((concat(x,y))) >= length(x)
• shape preservation, length(reverse(x)) == length(x)
• no errors given certain input, f(x) never throws if x > 0
• oracles, oldmethod(x) == newmethod(x)

Sometimes you can bake some more concrete logic into them like "doy(dt) should always give a number between 1 and 366".

Nice! Similar to one of the examples from this excellent talk from one of the creators of QuickCheck: https://youtu.be/zi0rHwfiX1Q

As for my own experience, I was trying to write tests for a process that matched entities between two data sets to find holes in the matches, with a complex bunch of rules and edge cases. The number of test cases I could imagine was fairly large (hundreds I'm pretty sure) but I really struggled to turn that into small, elegant "properties" like in the sibling comment. I suspect that the key difference is that I was not writing an elegant, computer-sciencey function with a concise definition and a difficult pragmatic implementation, but rather a messy business function that reflected our messy business logic.

I don't think that necessarily rules out PBT though. What I did find myself doing (similar to examples in the talk) is writing a "model" implementation that my real-world implementation could reference against, but ultimately stopped the exercise early as

• the real-world implementation was in the same high level language as the model implementation
• the real-world implementation was not hyper-optimised and didn't need to be

so I just didn't find the value in writing out the same thing twice in slightly different words, at least at that particular business