The thing that you didn't discuss in the above was the effect on the source code. Looking at your modified sources, I found it *significantly* harder to read your annotated version than the original. Basically every function and class was cluttered with irrelevant conditions, which obscured the logic and the basic meaning of the code.
My reaction was just the same as Paul's. I read the modified source, and found that the invariant declarations made it *dramatically* harder to read. The ratio was almost exactly as I characterized in a recent note: 15 lines of pre/post-conditions on a 10 like function.
Like Paul, I understand the documentation and testing value of these, but they were highly disruptive to the readability of the functions themselves.
As a result of reading the example, I'd be somewhat less likely to use a DbC library, and much more strongly opposed to having one in the standards library (and aghast at the idea of dedicated syntax)