Property-Based Testing with PropEr, Erlang, and Elixir

What you got here is one thing that make test-case generation tools (quickcheck, fuzzing) still useful even if you've done a full functional (platinum-level) proof of your program. Functional proof, at least in Spark, doesn't give you hard guarantees about running time, stack or heap space. So even after you've proved the absence of runtime errors in your deserializer, you might still be able to generate a test-case that blows the allowed stack size, or the available heap.

Some tools are starting to emerge, like gnatstack for Ada & Spark that gives (or tries to give you) the maximum stack size, statically - a parallel step to compilation, like the Spark examiner and prover). It's very limited in my opinion (some dynamic-sized object returned on the stack are not handled yet, function pointers, I don't have the list handy but it was quite limited). You can get similar stuff (less integrated) with gcc options, IIRC.

There's also all the work on WCET that might get interesting but modern architectures are so complex and changing that I'm not sure we'll get near ubiquitous, user-friendly availability for those tools in the near future (next 10 years). For the time being it's mostly used in 'hard' safety-critical projects (avionics), especially since multicore, deeply pipelined architectures, with shared resources (memory, cache, buses) are getting used more and more and they're harder to predict than the previous architectures.

I brought in the QuickTheories[0] library for property testing at work after being exposed to the articles here[1] (the final rule test is particularly interesting). My first use case was to test a generated parser for a restricted subset of the grammar for content security policy URLs, but I think this might be a bad use case since I'm not exactly testing "properties" so much as using the system for test data generation and quick code coverage. e.g. I have a test called something like testUrlPaths() that's mostly exercising the parser to make sure it doesn't forbid a valid but strange URL path that someone could enter. However while writing that test I discovered the parser was really doing the right thing, I found some violations with paths containing a '%' but not two hex digits immediately following. Unless I was writing unit tests for every bit of the grammar and paid attention to that part, I doubt I would have thought to test for them myself... Maybe the happy path of '%20' but not the fact that '%2' should be invalid. In the end I extracted those cases into three specific tests that will be there in case someone gets the funny idea to replace the validator with something not generated from a grammar (or generated from the wrong grammar), which isn't that unlikely since the spec allows for a lot more than what one might naturally consider allowing on your own (e.g. ftp resources).

Like with certain kinds of unit testing, I have the sense that the process of using a property testing framework has beneficial effects while a system is under development which aren't exactly clear to see from the artifacts of the final committed code and tests since by then you've dealt with a bunch of edge cases the tests told you about and have refactored / rewrote / removed things. So try it! Even if you don't commit it. And anyway the "trivial" problems are still worthwhile too (like catching errors in a pair of serializer/deserializer classes for some custom data), and like other kinds of tests it's best for your properties to be short and easy to read.

I think the chief difficulty is just adjusting to thinking in terms of "properties" that are worthwhile to check. The examples here[2] (and summarized in the quicktheories readme) are good starting points. Also it's more on the toy example side but I've personally made an analogy to Polya's How to Solve It introductory problem of finding the diagonal length of a box. He lists a bunch of other mathematically interesting things you can do with the solution besides just use it to solve the one problem, and most of those things could be encoded into properties. (Like, is the solution symmetric (shuffling around the box's length/width/height values doesn't change the answer), if you increase the height does the diagonal's length increase, if you scale all three sides does the diagonal scale the same amount, does it solve a related problem of the diagonal of a rectangle (box with height 0), are you using all the given data in the solution...) A point is that the math problem doesn't end with giving the answer, and similarly testing doesn't stop after you've verified the happy case or fulfilled some coverage requirement.

[0] https://github.com/ncredinburgh/QuickTheories/

[1] https://hypothesis.works/articles/intro/

[2] https://fsharpforfunandprofit.com/posts/property-based-testi...

I've been using my own property based testing framework https://johtela.github.io/LinqCheck/ for .NET projects and jsverify (https://github.com/jsverify/jsverify) for Typescript projects. Below are some repos using those:

https://github.com/johtela/Flop https://github.com/johtela/lamath

I can't point you to anything specific but here's something interesting: Linux filesystems, APFS, and FAT/NTFS have different parameters for legal filenames, so anything that must interop between multiple platforms should probably be property tested.

The Testimonials for Hypothesis lists projects where it was used successfully. https://hypothesis.readthedocs.io/en/latest/endorsements.htm...