3 ms·

This book is great! I was already familiar with the basics of property testing, but the book shows it can be used for way more than just the usual JSON parsing

This book is great! I was already familiar with the basics of property testing, but the book shows it can be used for way more than just the usual JSON parsing examples I had seen until now. In particular I liked the idea of negative testing: making sure bad things don't happen, even if you generate data from a wider domain than what a function is meant to support. The targeted property-based testing example is really impressive. The author tests a version of Quickcheck, and asks the framework to target a high runtime, putting an assertion in the test to make it fail if the runtime is very high. The framework then goes and generates an example of data causing O(n^2) behavior in quickcheck. Just beautiful. I'm not done with the stateful testing part, but already I applied some of the stuff to a Python project (using Hypothesis) with good results. I hope I get to apply it to Elixir in the future.

touisteur 8y ago
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.

touisteur 8y ago

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.