I really like having the Q&A in text so I can read through it without having audio to watch the video! I’m not sure how much effort it is for you to maintain though, feels like the sort of thing that could get exhausting to write quickly.
It’s not super-related to formal property verification, but I’ve been messing with bats lately to do some quick tests for one-off Python scripts that I write. It’s kinda like functional testing for bash scripts, verifying that certain lines are output and that the right error code is returned. Here’s a good tutorial, and here are some tests that I’ve written with it.
This is consistent with my experience on my last couple projects – using contracts along with property-based testing and/or fuzzing seems to have an especially high payoff (bugs found, with input that reproduces them) for the effort involved.
The property tests were conceptually all stateful tests – the test library (theft) generated and executed a sequence of API calls, updating a straightforward in-memory model of the thing under test along the way, and checked that the result from each API call made sense, based on the model so far. If the code and in-memory model ever diverged, or if any contracts* failed, then it found something worth further investigation. It also used shrinking to remove most of the irrelevant details from the input.
This approach is incremental, and combines well with other approaches – there’s no need to thoroughly cover everything in contracts before they start catching things. Properties can check the overall expectations of the code (“no series of valid operations leads to data loss”; “no input leads to pathologically bad performance”), but also the contracts will help catch tangential issues, like implicit assumptions about initialization. To some degree, contracts sidestep thinking about the overall properties of the code, because contracts will catch any inconsistencies uncovered by combining operations at random.
* Well, asserts, because this was in C – but I was using asserts for internal consistency contracts, not just p != NULL; and whatnot.
I really like having the Q&A in text so I can read through it without having audio to watch the video! I’m not sure how much effort it is for you to maintain though, feels like the sort of thing that could get exhausting to write quickly.
It’s not super-related to formal property verification, but I’ve been messing with bats lately to do some quick tests for one-off Python scripts that I write. It’s kinda like functional testing for bash scripts, verifying that certain lines are output and that the right error code is returned. Here’s a good tutorial, and here are some tests that I’ve written with it.
This is consistent with my experience on my last couple projects – using contracts along with property-based testing and/or fuzzing seems to have an especially high payoff (bugs found, with input that reproduces them) for the effort involved.
The property tests were conceptually all stateful tests – the test library (theft) generated and executed a sequence of API calls, updating a straightforward in-memory model of the thing under test along the way, and checked that the result from each API call made sense, based on the model so far. If the code and in-memory model ever diverged, or if any contracts* failed, then it found something worth further investigation. It also used shrinking to remove most of the irrelevant details from the input.
This approach is incremental, and combines well with other approaches – there’s no need to thoroughly cover everything in contracts before they start catching things. Properties can check the overall expectations of the code (“no series of valid operations leads to data loss”; “no input leads to pathologically bad performance”), but also the contracts will help catch tangential issues, like implicit assumptions about initialization. To some degree, contracts sidestep thinking about the overall properties of the code, because contracts will catch any inconsistencies uncovered by combining operations at random.
* Well, asserts, because this was in C – but I was using asserts for internal consistency contracts, not just
p != NULL;and whatnot.