True DbC

You understood simple DbC in C++ until yesterday’s entry. But, there are powerful features in true DbC. Let’s check it today. Features of DbC which you should pay attention to are the following.

  • Class invariants are inherited, that means that a derived class invariant will implicitly call the base class invariant.
  • For member functions in a class inheritance hierarchy, the precondition of a derived class function are OR’d together with the preconditions of all the functions it overrides. The postconditions are AND’d together.

In other words DbC works specially for hierarchy of a class. For class invariants inherited, you should write a derived class to call base class’ invariant. The page which this site introduces every days shows the following code:

void A::foo()


// B.h:

#include “A.h”

class B : public A {
#ifdef DBG
virtual void invariant()
{ …
void bar();

About precondition and postcondition, you should call these at in-line of the member function. But, in the deep class, it becomes very complex because you must call all conditions.

class B : A
#if DBC
int foo_preconditions() { …Bpreconditions… }
void foo_postconditions() { …Bpostconditions… }
int foo_preconditions() { return 1; }
void foo_postconditions() { }

void foo_internal()

virtual void foo()
assert(foo_preconditions() || A::foo_preconditions());

Can postcondition in C++ come true? Perhaps, it can’t. All of these specifications can’t come true in C++. Especially deep preconditions and postconditions aren’t able to use, because the code is too complex. But, you will not have to fulfill all these specifications. You had better handle only the specifications that you need well. Or you should make a preprocessor which automatically expand code.

This entry was posted in Uncategorized. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s