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()
{
check_invariant(*this);

check_invariant(*this);
}

// B.h:

#include “A.h”

class B : public A {
public:
#ifdef DBG
virtual void invariant()
{ …
contracts
A::invariant();
}
#endif
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
{
protected:
#if DBC
int foo_preconditions() { …Bpreconditions… }
void foo_postconditions() { …Bpostconditions… }
#else
int foo_preconditions() { return 1; }
void foo_postconditions() { }
#endif

void foo_internal()
{
implementation
}

public:
virtual void foo()
{
assert(foo_preconditions() || A::foo_preconditions());
foo_internal();
A::foo_postconditions();
foo_postconditions();
}
};


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.

Advertisements
This entry was posted in Uncategorized. Bookmark the permalink.

Leave a Reply

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

WordPress.com Logo

You are commenting using your WordPress.com 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 )

Google+ photo

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

Connecting to %s