4 ms·

Using invariants like this is now my preferred programming style. Almost all of my complex container classes have a dbg_check() method which checks all the inte

Using invariants like this is now my preferred programming style. Almost all of my complex container classes have a dbg_check() method which checks all the internal invariants hold, and panics if not. When testing and debugging, I’ll add calls to dbg_check() after each mutation of my data structure. And then I write a fuzzer which exercises my API in a loop. Each iteration, I check that my invariants still hold. The nice thing about this sort of invariant checking is that it makes it very fast and easy to narrow in on bugs. The crash happens right after a change which made the data invalid, not later when the invalid data is accessed. And a few dozen lines of fuzz testing can find an extraordinary quantity of subtle bugs. It’s remarkable. Devastating for the ego, but remarkable. Edit: Simple dbg_check implementation example: https://github.com/josephg/diamond-types/blob/3eb48478fd879e9f2bb9bcc6062762fbf2f8db21/src/causalgraph/check.rs https://github.com/josephg/diamond-types/blob/3eb48478fd879e... And here's a simple fuzz tester: https://github.com/josephg/jumprope-rs/blob/318e87d3aae1b2a0333042c7e75d30179c162f21/tests/test.rs#L202-L261 https://github.com/josephg/jumprope-rs/blob/318e87d3aae1b2a0...

SoylentYellow 4y ago
Do you have an example of this you can share?
- josephg 4y ago
  Updated the comment.
jandrewrogers 4y ago
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.
gavinray 4y ago
Invariants + property-tests/fuzz-tests (anything that does random generation/permutation) is a nuclear weapon Great stuff, thank you for sharing =D
gavinray 4y ago
Do you use the Cargo "contracts" for Design-by-Contract style invariants that plugs into Facebook's MIRAI prover thing? I always thought it this was super neat: https://crates.io/crates/contracts https://crates.io/crates/contracts https://github.com/facebookexperimental/MIRAI/blob/main/examples/shopping_cart/src/main.rs https://github.com/facebookexperimental/MIRAI/blob/main/exam... [dependencies] mirai-annotations = ... contracts = {version = "XXX", features = ["mirai_assertions"]}
- josephg 4y ago
  No I haven't seen that! On its own, I don't see much point in "contracts" annotation-style syntax - it looks like a complex solution to a problem I don't have. Whats so wrong with assert!() that we need to invent syntax. MIRAI looks wild though. Thanks for sharing!
intelVISA 4y ago
That's a really solid approach, as much as OO architecture in excess (Java) is grim I think it has a lot of merit for testing as hopefully your code is already organized to benefit from a lil fuzz. Hoping to try the new C++ contracts one day(tm).
throwaway9870 4y ago
"Writing Solid Code" pushes this type of checking and I have been using it for at least 20 years with similar effectiveness as you. I don't understand why such a simple and pragmatic method is so overlooked.
- _a_a_a_ 4y ago
  I can only agree, and Hoare's work on assrtions go back to the 80's (or even earlier?). We're in a bad place as devs when the bar is so pathetically low yet we still choose to crawl beneath it.
pjmlp 4y ago
Besides the usual sources like Eiffel, one Microsoft book actually did it for me, showing off the various uses of it on their products. "Code Complete: A Practical Handbook of Software Construction" So for those on Windows systems, a good way to do DBC for the last 20 years has been the various ASSERT_ variants, specially for MFC, https://learn.microsoft.com/en-us/visualstudio/debugger/c-cpp-assertions?view=vs-2022 https://learn.microsoft.com/en-us/visualstudio/debugger/c-cp... And the SAL annotations for security invariants, https://learn.microsoft.com/en-us/cpp/code-quality/understanding-sal?view=msvc-170 https://learn.microsoft.com/en-us/cpp/code-quality/understan...

SoylentYellow 4y ago

Do you have an example of this you can share?

josephg 4y ago
Updated the comment.

jandrewrogers 4y ago

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.

gavinray 4y ago

Invariants + property-tests/fuzz-tests (anything that does random generation/permutation) is a nuclear weapon Great stuff, thank you for sharing =D

gavinray 4y ago

Do you use the Cargo "contracts" for Design-by-Contract style invariants that plugs into Facebook's MIRAI prover thing? I always thought it this was super neat: https://crates.io/crates/contracts https://crates.io/crates/contracts https://github.com/facebookexperimental/MIRAI/blob/main/examples/shopping_cart/src/main.rs https://github.com/facebookexperimental/MIRAI/blob/main/exam... [dependencies] mirai-annotations = ... contracts = {version = "XXX", features = ["mirai_assertions"]}

josephg 4y ago
No I haven't seen that! On its own, I don't see much point in "contracts" annotation-style syntax - it looks like a complex solution to a problem I don't have. Whats so wrong with assert!() that we need to invent syntax. MIRAI looks wild though. Thanks for sharing!

intelVISA 4y ago

That's a really solid approach, as much as OO architecture in excess (Java) is grim I think it has a lot of merit for testing as hopefully your code is already organized to benefit from a lil fuzz. Hoping to try the new C++ contracts one day(tm).

throwaway9870 4y ago

"Writing Solid Code" pushes this type of checking and I have been using it for at least 20 years with similar effectiveness as you. I don't understand why such a simple and pragmatic method is so overlooked.

_a_a_a_ 4y ago
I can only agree, and Hoare's work on assrtions go back to the 80's (or even earlier?). We're in a bad place as devs when the bar is so pathetically low yet we still choose to crawl beneath it.

pjmlp 4y ago

Besides the usual sources like Eiffel, one Microsoft book actually did it for me, showing off the various uses of it on their products. "Code Complete: A Practical Handbook of Software Construction" So for those on Windows systems, a good way to do DBC for the last 20 years has been the various ASSERT_ variants, specially for MFC, https://learn.microsoft.com/en-us/visualstudio/debugger/c-cpp-assertions?view=vs-2022 https://learn.microsoft.com/en-us/visualstudio/debugger/c-cp... And the SAL annotations for security invariants, https://learn.microsoft.com/en-us/cpp/code-quality/understanding-sal?view=msvc-170 https://learn.microsoft.com/en-us/cpp/code-quality/understan...