Comment by josephg | Hacker News Reader

Comment by josephg | Hacker News Reader

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/3eb48478fd879e...

And here's a simple fuzz tester: https://github.com/josephg/jumprope-rs/blob/318e87d3aae1b2a0...

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.

> 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).

>> 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/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...

Hopefully Design by Contract can be included in the C++ standard itself in the future.

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.

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.

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-cp...

And the SAL annotations for security invariants,

https://learn.microsoft.com/en-us/cpp/code-quality/understan...

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://github.com/facebookexperimental/MIRAI/blob/main/exam...

  [dependencies]
  mirai-annotations = ...
  contracts = {version = "XXX", features = ["mirai_assertions"]}

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!

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).

"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.

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.

Invariants + property-tests/fuzz-tests (anything that does random generation/permutation) is a nuclear weapon

Great stuff, thank you for sharing =D

Do you have an example of this you can share?

Updated the comment.

Reply on news.ycombinator.com