Comment by teiferer
3 months ago
> a + b == b + a
> a + (b + c) = (a + b) + c
> a + (-a) == 0
Great! Now I have a stupid bug that always returns 0, so these all pass, and since I didn't think about this case (otherwise I'd not have written that stupid bug in the first place), I didn't add a property about a + b only being 0 if a == -b and boom, test is happy, and there is nothing that the framework can do about it.
Coming up with those properties is hard for real life code and my main gripe with formal methods based approaches too, like model checking or deductice proofs. They move the bugs from the (complicated) code to the list of properties, which ends up just as complicated and error prone, and is entirely un...tested.
Contrast that with an explicit dead-simple test. Test code doesn't have tests. It needs to be orders of magnitudes simpler than the system it's testing. Its correctness must be obvious. Yes, it is really hard to write a good test. So hard that it should steer how you architect your system under test and how you write code. How can I test this to have confidence that it's correct? That must be a guiding principle from the first line of code. Just doing this as an afterthought by playing lottery and trying to come up with smart properties after the fact is not going to get you the best outcome.
For the example it would be easily caught with PBT by testing the left and right identities for addition.
In general though, the advice is don't excessively dogmatic. If you can't devise a property to test, use traditional testing with examples. It's not that hard. Same way to deal with the problem of end-to-end tests or unit tests not being useful for certain things, use the appropriate test style and approach to your problem.
> Just doing this as an afterthought by playing lottery and trying to come up with smart properties after the fact is not going to get you the best outcome.
This sounds backwards to me. How could you write any tests, or indeed implement any functions, if you don't know any relationships between the arguments/return-value, or the state before/after, or how it relates to other functions, etc.?
For the addition example, let's say the implementation includes a line like `if (x == 0) return y`; would you seriously suggest that somebody writing that line doesn't know a property like `0 + a == a`? Would that only be "an afterthought" when "trying to come up with smart properties after the fact"? On the contrary, I would say that property came first, and steered how the code was written.
Incidentally, that property would also catch your "always returns 0" counterexample.
I also don't buy your distinction that "real life code" makes things much harder. For example, here's another simple property:
This is pretty similar to the `a + (-a) == 0` example, but it applies to basically any database; from in-memory assoc-lists and HashMaps, all the way to high-performance, massively-engineered CloudScale™ distributed systems. Again, I struggle to imagine anybody implementing a `delete` function who doesn't know this property; indeed, I would say that's what deletion means. It's backwards to characterise such things as "com[ing] up with smart properties after the fact".
I agree with you. However the grand-parent comment has a point that it's not easy to extract testable properties from code that's already written.
It's much easier to proceed explicitly like you suggest: have some properties in mind, co-develop property tests and code.
Often when I try to solve a problem, I start with a few simple properties and let them guide my way to the solution. Like your deletion example. Or, I already know that the order of inputs shouldn't matter, or that adding more constraints to an optimiser shouldn't increase the maximum, etc.
And I can write down some of these properties before I have any clue about how to solve the problem in question.
---
However, writing properties even after the fact is a learnable skill. You just need to practice, similarly to any other skill.
> However the grand-parent comment has a point that it's not easy to extract testable properties from code that's already written.
True, property-based testing does not solve the problem of deriving the intended behavior of code where behavior is not documented (either by requirements documents, or code comments, or tests that aren't just examples but clearly indicate the general behavior they are confirming, or...)
OTOH, PBT can be used to rapidly test hypotheses about the behavior (though intent is another question) of legacy code, which you are going to need to develop and validate to turn it into code that is maintainable (or even to replace it with something new, if you need to generally be compatible.) Determining whether deviations from a hypothesized behavior are intentional or bugs is still an exercise for the user, though whether the deviations are highly general or narrow to specific cases can help to illuminate that decision, and a library like Hypothesis will help determine that.
> Great! Now I have a stupid bug that always returns 0, so these all pass, and since I didn't think about this case (otherwise I'd not have written that stupid bug in the first place), I didn't add a property about a + b only being 0 if a == -b and boom, test is happy, and there is nothing that the framework can do about it.
Well, just add one example based test for eg 1 + 2 = 3, and you would catch this bug.
You can freely mix and match property based tests with example based tests.
> Coming up with those properties is hard for real life code and my main gripe with formal methods based approaches too, like model checking or deductice proofs.
Yes, property based testing is an acquired skill that has to be learned.
It's not so bad, once you've done it a few times, though.
It also changes how you design code in the first place. Just like even example-based testing changes how you design your code.
> They move the bugs from the (complicated) code to the list of properties, which ends up just as complicated and error prone, and is entirely un...tested.
You might be doing this wrong, if your list of properties is as complicated as the code. And it's not 'untested': you are exercising your properties against your code.
For a conceptually really simple example: suppose you have two different ways to solve a certain problem, and suppose neither is really simpler than the other. You still gain something from comparing the output of both approaches on random input: unless you made the mistake in both approaches, many bugs will show up as discrepancies that you can investigate. Hypothesis even includes 'shrinking' to helpfully provide you with a minimal counterexample that shows the divergence.
From a formal point of view, you can say that this property is 'untested'; but in practice you still gain something by comparing the two implementations.