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.
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.
>> 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:
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.
> 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).
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.
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.
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.
"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.
I thought "contracts" were dropped out of C++20.[1]
Entry and exit assertions, and invariants, are powerful, especially when coupled with a proof of correctness system. But they're a tough retrofit.
Invariants have some issues. The general idea is that the invariant has to be true when control is outside the object. This was once the core idea of the object concept, although it's been somewhat forgotten. A big issue is, when does control enter and exit the object? What if you call a public member function from inside the object? Did you re-enter? What if you call out of an object to something that calls back in? What about recursion? What if another thread enters? Objects need clarity on the inside/outside issue for invariants to work. This is quite possible but a tough retrofit.
Invariants need syntax for talking about arrays and parts therof. You need quantifiers, or something like them. Lambdas?
From back when I did this sort of thing, decades ago, a simple SAT solver can eliminate the need to check over 90% of assertions at run time. So you want something like that, rather than trying to check everything at run time. Otherwise, nobody will keep the checks turned on.
All this is quite do-able. Most attempts to do it have suffered from academic overreach - the technology is pushed by people in love with formal methods, and the result is too complicated for routine use.
> I thought "contracts" were dropped out of C++20.[1]
You're right, but (I'm not an authority, someone from /r/cpp would be better to speak here probably) I think after the Kona meeting recently they were back on the charter for next iteration
Specifically, GCC 13 has had support for Contracts in main since November:
> A big issue is, when does control enter and exit the object? What if you call a public member function from inside the object? Did you re-enter?
If you check the generated code from the end of the blogpost (see the bit that shows the Ghidra dissasembly) or the notes section, the pattern used in the plugin is:
T function() {
check_invariants(); // unless we're in constructor
result = function_body();
check_invariants(); // unless we're in a destructor
return result;
}
This does mean that a single member call can cause multiple cascading calls to check_invariants()
If "this.foo()" calls "this.bar()" which calls "this.baz()", etc.
But it's not avoidable, because in this open-world assumption we assume any member call can potentially mutate the state of the member.
If you're calling back into user code, you need to reestablish invariants first.
As for threading, C++ distinguishes mutating from non mutating (const) methods. Usually, any number of threads can call const methods simultaneously, but only one thread can have access if mutating methods are called. This may require external synchronisation.
The optimizer is often capable of inferring when invariants are maintained. One controversy is whether it should be permitted to use contracted invariants as axiomatic.
> What if you call a public member function from inside the object? Did you re-enter?
It's best to program as if every call to a public function is from client code (i.e. has the same pre/postconditions/invariants). If you need different semantics, it's straightforward to forward to a private or protected function to distinguish the two cases. This is similar to the Non-Virtual Interface (NVI) pattern.
When did you leave the object? There should be a check of the invariant as control leaves the object. At what moment does this happen.
The F# people struggled with this. In proof systems, you check invariants at exit, and get to assume them true at entrance. So you need to be very clear about entrance and exit.
> I thought "contracts" were dropped out of C++20.
C++ compilers often implement C++ features which haven't been fully standardized yet. Either to prepare for stuff that is very likely to be in the next version, or as experimental features so that people can try them out, find potential issues with proposal, and come to conclusion of what exactly should be standardized.
Contracts were not dropped from C++20 because people didn't want the feature. But at least partially because people had very different opinions of what exactly should they do (runtime checks, documentation to library users, optimization annotation giving permission to UB if input requirements aren't satisfied, hint for optional static analyzers).
Few years ago started using asserts as an ad-hoc documentation mechanism for invariants and then also started shipping them in production builds. When triggered, asserts grab the stack trace, write it into the application log and give an option of sending a bug report. And then they shut down the program.
Was scary at first, but the initial pain is absolutely worth it.
This flushed hundreds of absolutely crazy edge cases, improved code quality and stability tremendously. It also forced writing cleaner code to begin with and sped up debugging while in development. Now have about 3K asserts in 250 KLoC code base. Can't recommend this practice strong enough.
I believe Rust had some form of contract enforcement in its early days, but they eventually removed it because it had too many problems. I wish I could find the post about it, but Google is useless these days.
> The working code for insertion of the check_invariants statements was a stroke of dumb luck after 15 hours, from one of the suggestions given by Github Copilot.
GitHub Copilot coming in handy when documentation is lacking? Will widespread use of tools like this reduce the incentive, over time, to write good documentation? Something to think about.
I prototyped much of this code using ChatGPT and Copilot. I won't go so far as to say, "I couldn't have done it without you, ma!", but it certainly would have taken me much longer.
In terms of learning the actual API, they were worth their weight in gold.
One trick to use is that Copilot can read up to (apparently) 20 other tabs that you have open. So, I will open the source code containing the API methods I need in my other tabs and close everything else.
> The working code for insertion of the check_invariants statements was a stroke of dumb luck after 15 hours, from one of the suggestions given by Github Copilot.
What is funny here is that it suggested something radically different. I was going down the rabbit hole I chronicled here:
One strategy I use in unfamiliar territory is to repeatedly generate the set of 10 Copilot suggestions and see if anything sticks out. I had gone through maybe 3-4 rounds when it spits out one that looks nothing like what I currently have.
I try that suggestion, and it works. I shake my head. What the fuck. Alright, I'll take it.
It wanted to do a regular C-style call that had no member namespace, which by sheer luck happens to work due to how C++ lookup works.
One trick to use is that Copilot can read up to (apparently) 20 other tabs that you have open. So, I will open the source code containing the API methods I need in my other tabs and close everything else.
:shocked pikachu: This can’t possibly be true? How would it even do that, and unless it was off by default, that seems like a huge privacy problem. Edit: never mind, I was reading tabs as “browser tabs” not “editor tabs.”
Does anyone have an example of a codebase that uses Design By Contract to an extreme extent? You really only get a sense of the power of patterns like this when you see that power abused. I've greatly enjoyed writing 2 very small codebases in that style...but that doesn't mean I did it well or that it'd hold up after years of maintenance from a revolving door of developers.
Not the writer, but it seems obvious to me. It’s a luxury version of assert. You leave them enabled in debug builds to get better bug reports from testers.
Those testers may hit cases you forgot to write unit tests for.
Of course, you can also forget to write invariants, or write invariants that are less tight than they should be, but I think it often is easier to write invariants than to write exhaustive unit tests.
Firstly, writing “p should always be a prime” is clearer than writing “if p is a prime, and you call f, p should be a prime afterwards”, and secondly, invariants can apply to multiple methods that you, otherwise, would have to write separate tests for (“foo keeps p a prime”, “bar keeps p a prime”, “bar keeps p a prime when called with a null argument”, “baz keeps p a prime if it throws an exception”, etc)
Also, invariants, IMO, can be way better documentation than unit tests.
Finally, invariants leave open the possibility of using a theorem prover to (dis)prove that they hold.
They are declarative vs imperative and sufficiently smart tooling exists such that they can be checked and enforced statically, see liquid haskell and "refinement" typing for an example. Formal verification starts to become a possibility -- enforcing both conformance and documentation.
> What's the advantage of invariants over unit testing?
I studied Eiffel in university under Bertrand Meyer, and here's his (probably unique) point of view.
If someone hands you their library code and their unit tests, you have to understand their unit tests - which involves understanding why they chose the values that they did. There's also nothing stopping someone from testing the internals of their library as opposed to the publicly exposed behavior.
With contracts, imagine that to understand their library, you only see the method declarations with accompanying contracts. You don't see how HashSet.Add(x) is implemented, but you do see "if this.Contains(x) old(this.Count) == this.Count".
You don't have to see a test where this is tested with 5 example values, on an empty set, on a large set, whatever. You can rid yourself of that cognitive load by thinking, as sibling points out really well, declaratively over imperatively.
icontract is one implementation of Design by Contract for Python; which is also like Eiffel, which is considered ~the origin of DbC. icontract is fancier than compile-time macros can be. In addition to Invariant checking at runtime, icontract supports inheritance-aware runtime preconditions and postconditions to for example check types and value constraints. Here are the icontract Usage docs:
https://icontract.readthedocs.io/en/latest/usage.html#invari...
For unit testing, there's icontract-hypothesis; with the Preconditions and Postconditions delineated by e.g. decorators, it's possible to generate many of the fuzz tests from the additional Design by Contract structure of the source.
> icontract-hypothesis combines design-by-contract with automatic testing.
> It is an integration between icontract library for design-by-contract and Hypothesis library for property-based testing.
> The result is a powerful combination that allows you to automatically test your code. Instead of writing manually the Hypothesis search strategies for a function, icontract-hypothesis infers them based on the function’s [sic] precondition
This isn't a replacement for unit tests. This is an alternate syntax to using asserts. You would still want unit tests to see if those asserts are being violated.
The post assertions do look very similar to a unit test, but the pre assertions seem really useful; it can sometimes be difficult to know every code path that leads to your function, and though tools exist for this, assertions on inputs help you catch errors arising from unusual conditions.
This seems like it’s mostly syntactic sugar for assertions, keeping them at the interfaces of the function (in and out).
It can also be sometimes useful to have these conditions right there alongside the implementation and not just somewhere else in your unit tests.
Because this leads the way to being able to verify that your functions will act as expected in all cases, rather than just for the ones that you thought about when you were writing unit tests.
I believe I've read about some languages with invariant using them at compile time to verify the value meets the invariant, if possible. For example, let's say a function's invariant guarantees it returns an even integer, and then we pass that into a function that only accepts odd negative integers, it could catch that during compile time. To me, that's the coolest case for invariants.
Again, I believe that this is a PL research topic, but I'm not super well versed in it, so take that with a grain of salt.
Invariant vs unit tests aside. Doesn't this being a gcc plugin make it inherently unattractive? Wouldn't want to have to rip that code out if I wanted the code to behave on a non-gcc toolchain.
Otherwise, seems cool if that doesn't matter / will never matter in the lifetime of the codebase
> Doesn't this being a gcc plugin make it inherently unattractive?
I'm the author, and even I think so. I'm more of an LLVM fan myself (though I can't not mention David Malcom's work on the GCC Static Analyzer).
(Ideally it wouldn't be a plugin at all, it'd be a language feature. We got Contracts and left out the most useful contract of them all)
Originally, I started it as a Clang plugin, thinking that I could also implement support for the Contracts "[[pre]]" and "[[post]]" specification on top (or at least some minimal implementation of it).
This turned out to be a lot more work.
If people would like to use this from Clang, even without support for regular Contracts, I will publish a compatible Clang plugin.
I think at some point there was support for Contracts in Clang, maybe longer term I'll try to get them working again? (I've no experience here)
That is a concern, but this makes invariants something the compiler can reason about more easily, since they happen at function boundaries and are distinct from regular code, unlike “vanilla” assertions.
Would be nice to have a non-macro solution for controlling behavior at configure time, but the `NDEBUG` macro is basically already your `DEBUG` constexpr.
Better to define a macro that evaluates to the contract/invariants on GCC and empty on other compilers, rather than copying the ifdef/else/endif logic around to every usage.
The B-Tree invariant example in the unit test seems like a bunch of assertions. Feels very similar to unit tests? Am I missing something?
Assert at runtime or assert at unit test time, it's assertions all the way down? Not sure the benefit of some weird @decortator-like syntax to achieve 5-10 lines of assertions?
Contracts and Invariants don't replace unit tests, they're complementary
This is the big mix up with DbC in general I think. Think of it more like sanity-tests and assertions that help ensure your program isn't in some haywire state.
A good example with the BTree is that the invariants ensure the properties are enforced at runtime, but you still need test to invoke those properties.
These sorts of invariants mix really well with property-style tests:
You write some declarative specification for a set of boundaries on inputs/outputs, and then subject your classes to the generated inputs. If your tests pass, then all your invariants have held and you know at the bare minimum, the data structures are doing what you intend them to do.
Above that you can do load-testing and subject the invariants to scale-factors.
If I remember well(), the idea between contracts is that they can be enabled at runtime, so very different from UT.
Also different from assertions in that 'class' invariants applies to every public method of the class.
: All I know about 'Design by Contract' I learned it in the (very good IMHO) book Object Oriented Software Construction by Bertrand Meyer (he made the Eiffel language).
D has had support for pre/post contracts and invariants for a long time, but I haven't seen them used in many projects. I think it's one of those niche uses, or something that sounds like it'd be fun to have but in the end ends up being annoying to maintain.
Creating a separate gcc plugin for this seems unnecessary if I am not misunderstanding something. Just ensure the invariant function is called at every method, in debug builds maybe. You could of course change the object properties without using a method but then you have bigger problems.
Yeah you totally could, and before writing this plugin it's what I was doing, haha. As there is a human involved, it is very error prone though, and boy is it tedious!
A big part of DbC is that contracts are part of the public interface, not the implementation. This becomes especially important once you mesh them with Simula-style OOP, as derived classes need a way for overridden methods to widen or narrow the inherited contract.
In other languages adding something like this is possible from within the language in basically any syntax you want. No need for some plugin on another layer like GCC.
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...