Property-Based Testing

Property-based testing. What’s interesting about it is that, compared with traditional tests, it doesn’t need to exhaust everything. Or put it this way: at the level of the spec, the area it covers is “universal within the property”. Logically, if you define a correct property, it takes in the whole set of possibilities within that range. It doesn’t guarantee a 100% hit by itself, of course, and its advantage mostly comes from the comparison with single-point tests. You can see the lack of a guarantee from how it works. Once the property defines what counts as correct, you need to build a generator that keeps firing random inputs and checks whether the results land in the specified correct range. Its core idea is sampling, and that means there will always be places it doesn’t cover.

First, a word on Daniel Jackson’s SCH (small scope hypothesis). The idea is that for a given false assertion, there’s almost always a minimal counterexample, and for errors caused by the structure of the implementation, we only need to enumerate exhaustively within a small scope to find them. The classic example is permissions. You don’t need to simulate hundreds or thousands of users. The problems permission interactions can cause show up once a single-digit number of permissions interact back and forth. Most bugs don’t necessarily need scale to appear (of course that’s an empirical judgment, and there are bugs that really only happen past a certain scale); they tend to show up at small scope.

OK, so with that, why use PBT at all? The problem is the exhaustive enumeration. Make the scope even a little bigger and the space explodes, and you also have to write it in a formal language like Alloy. Its advantage is that once it finishes it really can “prove” there’s no counterexample within that scope, but the cost is on the high side. PBT swaps bounded exhaustive enumeration for random sampling, so we get SCH’s benefit without having to enumerate everything. The price, of course, is giving up exhaustive proof in the universal sense, but the trade is worth it.

PBT suites have a very handy operation called shrink. I said above that SCH says false assertions usually have small counterexamples, but with sampling, once you find an error, how can you say it’s a small counterexample for the current sample? Shrink is there to find that small counterexample. After it finds an error, the suite keeps trying to shrink the failing input. Say you get something like (733921845, -2147483648), an error that’s hard for a human to make sense of (too big, too broad). It keeps trying to shrink toward zero, and when it’s done it stops at a minimal failing value. (0,0) passes but (-1,0) fails, and we can see right away the error is about the sign, not just the size of the number. Note that the shrinking goes by type: arrays drop elements, strings get shorter. One way to see it is as an engineering technique that keeps ruling things out until it gets close to the minimum, and usually the simpler it is, the easier it is for a person to understand. So if PBT finds an error, traditional example tests still come in as a supplement here. After shrinking, pin it down with a minimal regression test.

Frankly, like Property-based testing is about to rule the (software) world says, PBT really is pretty niche, but it’s going to matter more and more in the era of AI development. The reason is that generation is getting faster than verification, and our code is gradually turning into a black box. How do I guarantee the quality of a black box? The testing setup we already have can do it, of course, but efficiency is always a bottleneck. Take example-based testing: I (well, these days the tests are written by AI too) have to rack my brain for cases that might go wrong, and that’s exactly where the limit is. What if I don’t think of it?

The root cause is that traditional testing asks you to think about what “you can think of”, but the problems sit exactly in the places “I can’t think of”. This is almost a truism (or a paradox?), because anything I can think of stops being a problem. If I thought of it, why wouldn’t I add it? Well, most of the time I can’t exhaust everything. My experience and energy limit how far I can think, and even AI can’t do it. They have endless memory, but context and attention are limited too, and the set of possibilities they consider is noticeably bounded by the range of input they get.

That’s the problem PBT is for.

Writing it is a bit counterintuitive. When we write normal test cases we’re thinking about the “concrete” implementation, but writing a property asks you to think about the “shape”. Or in logic terms, we need to think in universally quantified definitions. Set theory makes it more intuitive: {1,4,9,16} and {n² | n ∈ ℕ}. The first covers only four elements, but the second covers every n ∈ ℕ. That’s drawing the range.

Take 1+1=2:

// traditional: three instances of the axioms
expect(add(1,1)).toBe(2);
expect(add(2,3)).toBe(5);
expect(add(0,7)).toBe(7);

// PBT: the axioms themselves
fc.assert(fc.property(fc.integer(), fc.integer(),
  (a,b) => expect(add(a,b)).toBe(add(b,a))));           // commutativity
fc.assert(fc.property(fc.integer(),
  (a) => expect(add(a,0)).toBe(a)));                     // identity element
fc.assert(fc.property(fc.integer(), fc.integer(), fc.integer(),
  (a,b,c) => expect(add(add(a,b),c)).toBe(add(a,add(b,c))))); // associativity

This defines the correct boundary of addition straight from the rules. If the addition I write ever breaks these rules, it’s definitely wrong.

Then again, the example above has a trap in it. I didn’t catch it at first either, I only noticed during an adversarial review afterwards. The example satisfies the textbook axioms of addition perfectly, but it’s too big a shape. Pass in a bitwise operation like a|b, for instance, and it can’t catch the case where the calculation is wrong. And it’s well hidden. The bitwise op passes fine within the current test scope, and when there’s no carry the output doesn’t even differ from normal addition. But once a carry is involved, the result is wrong. 4|3 in binary is 100 and 011, giving 111 = 7; 5|3 is 101 and 011, and the result is still 7, but the correct result should be 8. So you should add the cancellation law too, i.e. a+c ≠ b+c where a≠b. Then in bitwise terms 1|1 = 1 and 0|1 = 1 turn the test red right away. Even so, something is still left uncovered: XOR still satisfies the current properties and gives unexpected results while everything is green (1^1 = 0, but it should be 2). But this is where the trade-off comes in, and what matters is which shape fits the business best. I’d even say that normally you don’t need to add the bitwise case at all, since regular business code never has bitwise operations anyway. But the example does show that even an “axiomatic property” you think is complete enough will have blind spots you didn’t think of. Here the shape is drawn too big. Normal addition, bitwise OR and XOR all fit inside it, plus a lot of other stuff the business shouldn’t include. Example tests only show this at single points, while PBT here is our definition of the shape of the relation. Added afterwards, looking back

Once the rules are defined, you run it a lot: generate random a, b, c, feed them into the implementation under test, and check whether the results follow the rules. This naturally brings up where it applies. Because PBT relies on lots of coverage to approach the universal, it’s a bad fit for anything that needs real time to produce a result. Take DOM rendering. If every run has to render once, fire enough of them and the time balloons past what you can put up with.

Second, precisely because of this randomness, PBT isn’t deterministic from run to run. The random inputs differ every time, and exploring this part of the space this time doesn’t mean next time will be exactly the same. I’m exploring new areas where errors might hide, and having mapped out this part doesn’t mean I’ve mapped out all of it. But since each run has a seed, reproducing a known error once isn’t that hard.

PBT doesn’t work in every situation, though. One case is when correctness depends on external state (say a specific magic number, or a semantic constraint) and is guaranteed by convention. When correctness is defined by a lookup table rather than by the structure of relations, PBT doesn’t gain much (or what you end up with is barely different from example-based tests). Correctness was hard-coded from the start, so you might as well go straight to example tests. Another case is single-point results a random generator probably won’t hit. This is actually similar to the first. When only one exact value is correct, broad PBT is redundant, since everything the generator fires besides that point is wasted. Why not just test that single case?

PBT can cover a wide range, but you can also see that how hard it searches for bugs is decided from the start by the properties and generators we build ourselves. That part still needs a person to think it through, and if a bug happens to sit outside the covered range, PBT still won’t catch it. Though to be fair, values like that shouldn’t be tested with PBT in the first place. PBT shines where there are lots of combinations, because example tests are always single points while PBT works over ranges. So in terms of probability, its chance of catching bugs you didn’t think of is far higher than single points.

You can see from this that PBT as a testing method ends up constraining the implementation in return. For code to be testable with PBT, it has to cut its dependence on external state as much as possible (like I said above, depending on externally agreed state makes PBT close to the same thing as example tests), and keep a single responsibility (the structure has to be stable before you can draw its range, and if it’s too mixed you can’t draw it at all). That’s exactly why I think it fits the AI era so well. It turns around and constrains what the AI does.

But to hold back the AI’s tendency to change code just to satisfy the tests, you still need to watch the following:

• PBT properties have to be drawn at the outermost layer, meaning on the core functions, not padded out with helper functions.
• They have to survive mutation testing and adversarial review. Otherwise shooting the arrow first and painting the target around it, making up a shape that happens to pass, still works with PBT. And PBT has a cost under mutation: every run fires a lot of random inputs, which makes a full mutation run slower.
• Order. The discipline I currently argue for, tests first and code after, still has to hold. The shape has to be fixed up front, then you write the code. At bottom, tests are there to pin down the business logic, and only after thorough discussion, once the AI has been told clearly what the “correct shape” is, will the code that comes out be usable.
• You need to be clear about when you can skip PBT. Like I said above, some things are fine with example tests, and PBT there is plain unnecessary. Agreed-upon values, SQL, that kind of thing. If the AI forces these pre-fixed shapes into PBT anyway, it’s pure redundancy and a net loss.

Back to where I was: all in all PBT isn’t a cure-all, and it has quite a few traps. As the business domain gets more complex, for example, the generators get more complex too. There’s also the time cost of all the random firing, since one test run takes longer as generation gets more complex. Its core use case is relationships where combinations might explode, like when lots of different combinations make example-test coverage extremely tedious. Sequences of user actions in UI interaction tests belong here too. Overusing PBT can be a net loss. Lots of random generation and operations end up just slowing the tests down, or even producing a pile of fake greens that only give you peace of mind.

---

Translation note. I wrote this in Chinese. This English version is an LLM translation, so the wording is not mine even though the thinking is. Original: 基于属性的测试.