@tomekowal - Software Developer at ClubCollect
Introduction to stateful property based testing
Talk in three words: Stateful Property-Based Testing
Abstract
Property-based testing is a technique for writing tests that use a framework for creating test inputs and user-defined properties for validating outputs. Generating data allows for finding bugs that would be impossible to catch by regular unit tests: e.g. too big to encode by hand. This talk will explain why it is worth getting into PBT by introducing successful usages of PBT for testing AUTOSAR, LevelDB and Dropbox. All these examples use stateful testing, so the second half of the talk describes steps to create a stateful test for a simple key-value store.
Objectives
Introductory materials for PBT often focus on straightforward cases which are great for teaching but fail to show the true potential of PBT. The goal of this talk is a high-level overview that is both encouraging for beginners but also maps the road to mastering Property-Based Testing.
Audience
Developers who have heard about Property-Based Testing but are not convinced yet about its usefulness.
The speaker
Tomasz has worked with functional languages for over eight years and loves learning and teaching about concepts and techniques.
All will be added to the ElixirConf EU 2019 Talks List or via the #elixirConfEU2019 tag.
6 Likes
Really enjoyed the talk, @tomekowal! I’ve found PBT incredibly helpful for pure operations like confirming values roundtrips through serialization and deserialization. I haven’t taken the plunge into stateful PBT yet, but your PESEL example and points about identifying useful command generators for the domain was helpful.
Requirements involving time+state generally seem challenging to test. For example, suppose a server maintains session data for each client for at least 60s since the most recent request from that client, and within 90s of no requests deletes session data for that client. These timers are long enough that PBT, or any other tests, would discourage developers from using them. Generating commands which simulate some duration passing before the following command would help, but to benefit from it the system under test needs to support jumping forward in time.
Anyone have experience structuring code to support fast PBT testing with timers, while also preventing unintentional time simulation in the production environment? I understand sometimes people use model checkers like TLA+ for this, but like @tomekowal I’m unsure whether shrinking would work and there’s still the matter of faithfully translating and maintaining correspondence between the abstract model and the actual implementation.
Excuse me while I go order Fred’s latest book. 
If you’re testing with timers then you’ll want to add the timers to the model itself. After all time is part of your state at that point. You can treat timer calls as a command to generate. This allows you to deterministically control your tests and consequently run them much faster. It also allows you to induce weird failures that you wouldn’t normally see (like firing timers in incorrect orders for instance). I typically do this by shimming the timer module. My SUT uses the shim. In production it’ll use the real timer module. In my tests they’re just dummy calls.
3 Likes
Is that a standard cache?
I am not sure I would use PBT for such case. It makes sense where there is an explosion of different states. In case of cache, there are two: the data is there, or it isn’t.
Other argument for not testing it this way is that usually after deleting the session, you fetch it from the DB or somewhere else. It doesn’t affect how your system behaves to the outside world. It is an implementation detail that can you should leave out of model.
If there is other stuff depending on it, and you want to test it with PBT, you can pass current time to the functions as an argument. That makes it easier to test in general - not only for PBT
2 Likes
That’s not what I had in mind, but those are good points.
Oh that makes sense–thanks.
The example requirement was intended as an explicit feature of the server API. Although clients can’t be sure data isn’t retained longer without being able to audit the running code, they can at least know the server behave as if they have a clean slate after waiting >70s. The PBT would help in case this guarantee ever needed to be audited and help maintain the guarantee as the implementation evolves.
Another potential reason for the requirement is avoiding per connection session data becoming a memory leak.
1 Like
