Tuesday, April 18, 2006

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.

No comments: