For code that's more "business logic" rather than "algorithmic", I find the following helpful:
- Despite the terrible tutorial examples, PBT isn't about running one function on an arbitrary input, then trying to think of assertions about the result. Instead, focus on ways that different parts of your production code fits together, what assumptions are being made at each point, etc.
- You don't need to plug random inputs directly into the code you're testing. There are usually very few things to say regarding truly arbitrary inputs, like `forAll(x) { foo(x) }`; but lots more to say about e.g. "inputs which don't contain Y" (so run the input through a filter first), or "inputs which don't overlap" (so remove any overlapping region first), and so on.
- Don't focus on the random inputs; the whole idea is that they're irrelevant to the statement you're asserting (it's meant to hold regardless of their value). Likewise, if your unit test contains some irrelevant details, use PBT to generate those parts instead.
- It's often useful in business-type software to think of a "sequence of actions" (which could be method calls, REST endpoints, DB queries, or whatever). For example, "any actions taken as User A will not affect the data for User B". Come up with a simple datatype to represent the actions you care about, write a function which "interprets" those actions (i.e. a `switch` to actually call the method, or trigger the endpoint, or submit to query, or whatever). Then we can write properties which take a list of actions as input. Remember, we don't need to run truly arbitrary lists: a property might filter certain things out of the list, prepend/append some particular actions, etc.
- Once we have some assertion, look for ways to generalise it; for example by looking for places to stick extra things which should be irrelevant.
As a simple example, say we have a function like `store(key, value)`; it's hard to say much about the result of that on its own, but we can instead say how it relates to other functions, like `lookup(key)`:
forAll(key, value) {
store(key, value);
assertEqual(lookup(key), Some(value))
}
Yet we don't really care about lookups happening immediately after stores, we want to make a more general statement about values being persisted:
forAll(key, value, pre, suf) {
runActions(pre) # Storing shouldn't be affected by anything before it
store(key, value)
runActions(suf.filter(notIsStore(key))) # Do anything except storing the same key
assertEqual(lookup(key), Some(value))
}