3 ms·

I do something very similar, and as you say it is highly effective. I don't recall ever finding a bug later in code that was properly tested this way. It is no

I do something very similar, and as you say it is highly effective. I don't recall ever finding a bug later in code that was properly tested this way. It is not an inexpensive type of testing when done well but I think it is a pragmatic way of producing code that can approach the robustness of formal verification in practice with a lot less work, so the ROI is high.

josephg 4y ago
> It is not an inexpensive type of testing when done well I find the ROI is much higher than most forms of unit testing. Fewer lines of testing code finds more bugs. And with invariant checking and a seeded random number generator, you can reproduce any failures and (usually) find the bug pretty quickly. They do take more brain cells per line of testing code though, especially at first. This sort of testing also addresses my biggest frustration with unit testing. Unit tests have diminishing returns as you add more tests. Normally by the time I have "enough" unit tests, it becomes exhausting to refactor my code because of the giant pile of tests I need to rewrite. Fuzz tests are much easier to update. (That said, fuzz testing can't replace unit tests entirely. Especially when you have a lot of methods in your API).
thesuperbigfrog 4y ago
>> I think it is a pragmatic way of producing code that can approach the robustness of formal verification in practice with a lot less work, so the ROI is high. This is correct. Design by Contract techniques help to ensure that code is robust and works as expected. It is good that C++ is getting these tools through compiler plug-ins. The Ada programming language added support for Design by Contract in Ada 2005: https://learn.adacore.com/courses/intro-to-ada/chapters/contracts.html https://learn.adacore.com/courses/intro-to-ada/chapters/cont... The same language syntax used to define preconditions, postconditions, and invariants in Ada paved the way for SPARK to prove program correctness: https://learn.adacore.com/courses/intro-to-spark/chapters/03_Proof_Of_Program_Integrity.html#contracts https://learn.adacore.com/courses/intro-to-spark/chapters/03... Hopefully Design by Contract can be included in the C++ standard itself in the future.
- pjmlp 4y ago
  It almost made it into C++20 and was dropped at the last minute, I doubt it ever does again unless everyone agrees, even then, it is at least a decade away.
_a_a_a_ 4y ago
Good as DBC/assertions are, it absolutely does not "approach the robustness of formal verification in practice" especially for potentially large states. Also DBC/assertions are of little value unless you provide test code to exercise that asserted section, so that's more work, unless you're ok with the assertion triggering by the user after you've shipped it. Also comprehensively asserted code (with assertions switched on / compiled in) can absolutely crawl because preconditions that formal verification ensures have to be repeatedly checked at runtime - that's your assertion being run ten thousand times instead of being known-true in the code. It is very good, I use it extensively, but it is not even comparable to formal proofs. Nowhere near.

josephg 4y ago

> It is not an inexpensive type of testing when done well I find the ROI is much higher than most forms of unit testing. Fewer lines of testing code finds more bugs. And with invariant checking and a seeded random number generator, you can reproduce any failures and (usually) find the bug pretty quickly. They do take more brain cells per line of testing code though, especially at first. This sort of testing also addresses my biggest frustration with unit testing. Unit tests have diminishing returns as you add more tests. Normally by the time I have "enough" unit tests, it becomes exhausting to refactor my code because of the giant pile of tests I need to rewrite. Fuzz tests are much easier to update. (That said, fuzz testing can't replace unit tests entirely. Especially when you have a lot of methods in your API).

thesuperbigfrog 4y ago

>> I think it is a pragmatic way of producing code that can approach the robustness of formal verification in practice with a lot less work, so the ROI is high. This is correct. Design by Contract techniques help to ensure that code is robust and works as expected. It is good that C++ is getting these tools through compiler plug-ins. The Ada programming language added support for Design by Contract in Ada 2005: https://learn.adacore.com/courses/intro-to-ada/chapters/contracts.html https://learn.adacore.com/courses/intro-to-ada/chapters/cont... The same language syntax used to define preconditions, postconditions, and invariants in Ada paved the way for SPARK to prove program correctness: https://learn.adacore.com/courses/intro-to-spark/chapters/03_Proof_Of_Program_Integrity.html#contracts https://learn.adacore.com/courses/intro-to-spark/chapters/03... Hopefully Design by Contract can be included in the C++ standard itself in the future.

pjmlp 4y ago
It almost made it into C++20 and was dropped at the last minute, I doubt it ever does again unless everyone agrees, even then, it is at least a decade away.

_a_a_a_ 4y ago

Good as DBC/assertions are, it absolutely does not "approach the robustness of formal verification in practice" especially for potentially large states. Also DBC/assertions are of little value unless you provide test code to exercise that asserted section, so that's more work, unless you're ok with the assertion triggering by the user after you've shipped it. Also comprehensively asserted code (with assertions switched on / compiled in) can absolutely crawl because preconditions that formal verification ensures have to be repeatedly checked at runtime - that's your assertion being run ten thousand times instead of being known-true in the code. It is very good, I use it extensively, but it is not even comparable to formal proofs. Nowhere near.