Re: [boost] [dbc] Interest in Design By Contract for C++?

Subject: Re: [boost] [dbc] Interest in Design By Contract for C++?
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2009-10-27 10:33:10

Hello all,

The "EXAMPLE WITHOUT MACROS" below shows how to use this library to write
contracts WITHOUT using the foreign looking macro-based API. This example
should be used to understand how this library API actually works without the
obscure "macro magics".

***To all Boosters: Your comments are welcome!***

EXAMPLE WITH MACROS
-------------------

I presented this example for C++ in a previous email (it was originally
written by [Mitchell2002] for Eiffel).

As indicated in previous emails on naming conventions, if this library were
to be added to Boost:
1) All macros will be prefixed with BOOST_ and all names will be in the
boost:: namespace.
2) All names will be fully spelled (..._MEM_FUN -> ..._MEMBER_FUNCTION,
etc).
3) DBC/dbc might be replaced by CONTRACT/contract.
4) The need for ..._INHERIT_OBJECT and dbc::object<> might be removed (not
sure yet).
5) "DBC_COPYABLE(type)" and "DBC_BASE(type)" might be replaced by
"(copyable)(type)" and "(inherit)(type)".

// File: RelaxedNameList.hpp (using macro-based API).

#include <dbc.hpp> // This library.

class RelaxedNameList: public NameList
        DBC_MULTI_INHERIT_OBJECT(RelaxedNameList) {
public:
    void put(const std::string& name)
    DBC_MEM_FUN( (public) (void)
            DBC_COPYABLE(RelaxedNameList)DBC_BASE(NameList)
            (put)( DBC_COPYABLE(const std::string&)(name) ), {
        // Preconditions.
        DBC_ASSERT_STREAM(self.has(name), "in list",
                err << "name '" << name << "' not in list");
    }, {
        // Postconditions.
        if (self.old.has(name.old))
                DBC_ASSERT(self.now.count() == self.old.count(),
                "if in list, count unchanged");
    }, ; /* Body -- ';' separates definition from declaration. */)

    ... // Rest of this class.

private:
    DBC_INVARIANT(RelaxedNameList, {
        // Class invariants.
    })
};

// EOF

// File: RelaxedNameList.cpp (using macro-based API).

#include "RelaxedNameList.hpp"

void RelaxedNameList::DBC_BODY(put)(const std::string& name) {
    ... // Function implementation.
}

// EOF

EXAMPLE *WITHOUT* MACROS
------------------------

This is the example above but written without using the library macro-based
API. Not using the macro-based API requires programmers to write quite a bit
of setup code and it is not recommended (also the automatic contract
documentation and other library features are only supported when the
macro-based API is not used).

The example's lines are numbered (1), (2), etc and (long -- sorry ;) )
explanation text is given below. Most of the library requirements listed
below were derived from Eiffel's specifications for DBC and from a proposal
to the C++ standard committee for adding DBC to C++ (see [Meyer1997] and
[Ottosen2004] cited in previous emails).

// File: RelaxedNameList.hpp (NOT using macro-based API).

#include <dbc.hpp>

class RelaxedNameList: public NameList
// Instead of the DBC_MULTI_INHERIT_OBJECT macro:
#ifdef DBC
        , private dbc::object< RelaxedNameList > // (1)
#endif // DBC
        {
public:
    void put(const std::string& name)
// Instead of the DBC_MEM_FUN macro:
#ifdef DBC // (2)
    {
        dbc_contract_put_name().call(*this, &RelaxedNameList::dbc_body_put,
                name, "put"); // (3)
    }
protected: // (4)
    // (5)
    friend class dbc::fun<void, dbc::copyable<const std::string&> >::mem<
            dbc::copyable<RelaxedNameList>,
NameList::dbc_contract_put_name>;
    friend class dbc::post<NameList::dbc_contract_put_name::class_type>;
    friend class dbc_contract_put_name; // (6)
    class dbc_contract_put_name: // (7)
            public dbc::fun<void, dbc::copyable<const std::string&> >::mem<
// (8)
            dbc::copyable<RelaxedNameList>, NameList::dbc_contract_put_name>
{
        void require(const RelaxedNameList& self, const std::string& name) {
// (9)
            // Preconditions.
            DBC_ASSERT_STREAM(self.has(name), "in list",
                    err << "name '" << name << "' not in list");
        }
        void ensure(const dbc::post<dbc::copyable<RelaxedNameList> >& self,
                const dbc::post<dbc::copyable<const std::string> >& name) {
// (10)
            // Postconditions.
            if (self.old.has(name.old))
                    DBC_ASSERT(self.now.count() == self.old.count(),
                    "if in list, count unchanged");
        }
    };
    void dbc_body_put(const std::string& name)
#endif // DBC
    ; // (11)
public: // (12)

    ... // Rest of this class.

private:

// Instead of the DBC_INVARIANT macro:
#ifdef DBC
    friend inline void DBC_INVARIANT_FUN_NAME(const RelaxedNameList& self) {
// (13)
        // Class invariants.
    }
#endif // DBC
};

// EOF

// File: RelaxedNameList.cpp (NOT using macro-based API).

#include "RelaxedNameList.hpp"

void RelaxedNameList::
// Instead of the DBC_BODY macro:
#ifdef DBC // (14)
    dbc_body_put
#else // DBC
    put
#endif // DBC
        (const std::string& name) {
    ... // Function implementation.
}

// EOF

(1) If the class is already inheriting from other classes then this line
must start with "," (like in this example) otherwise it must start with ":"
(this is what the two macros DBC_MULTI_INHERIT_OBJECT and DBC_INHERIT_OBJECT
do). The inheritance is private so not to alter the public inheritance tree.
The base class dbc::object<C> is of a different type for every class C so
not to introduce a single common ancestor to all classes.

*NOTE* It was a requirement to not change the public inheritance tree and to
not introduce common ancestors.

(2) The actual library implementation uses more granular #ifdef than just
"#ifdef DBC" so to remove compilation of contracts entirely, or only
preconditions, or only postconditions, or only invariants, or any
combinations of the above. For simplicity, this example only uses "#ifdef
DBC" which allows to entirely remove contracts from compilation.

*NOTE* Read the example above thinking that ``DBC'' is #undef -- you will
see that the class code looks EXACTLY like if there were no contracts at
all. When "#undef DBC" the contracts overhead is _completely_ removed from
compile-time, run-time, and object files size. This was a requirement.

(3) dbc_contract_put_name::call() (inherited from dbc::fun::mem::call())
implements the DBC call semantics checking invariants and preconditions,
executing the body, checking invariant and postconditions (see previous
emails for DBC call semantics definitions):

    Function-Call := {Inv AND Base-Inv AND (Pre OR Base-Pre)} Body {Inv AND
Base-Inv AND Post AND Base-Post}

call() arguments are:
    A reference to the object (*this) -- the object reference is constant
only for constant member functions.
    A function pointer to the body (dbc_body_put).
    The arguments (name) -- these are of the function argument types (a
string constant reference in this case).
    A optional string describing the function's name (for error reporting in
case of a contract violation).

Preconditions, postconditions, and invariants are checked executing
require(), ensure(), and DBC_INVARIANT_FUN_NAME() functions (see below). If
these functions do not throw, terminate, or exit, the conditions they are
checking are considered passed.

*NOTE* It was a requirement to properly handle constant member functions.

(4) The contract class and the body member function are protected so
contracts do not alter the class public API. (They need to be protected and
not private to allow eventual deriving classes to subcontract from
RelaxedNameList...)

*NOTE* It was a requirement to not alter the class public API.

(5) However, (4) requires to make some of the library classes friends. (This
may generate a "duplicate friend" warning on some compilers...)

(6) This friend is not needed on modern C++ compilers (that implement the
fix for C++ standard defect "45. Access to nested class", see
http://www.open-std.org/jtc1/sc22/wg21/docs/cwg_defects.html) but it is used
anyway to ensure backward compatibility with older compilers -- it does not
hurt.

(7) The contract class name contains both function and argument names to
allow contracts to work for overloaded functions (with some limitations
because C++ overloading is based on argument types and not their names...).
Contracts can also be written for operators but the operator symbol must be
spelled-out with words in the contract name -- for example, for "T
opreator[](const size_t& index)" the contract class name can be given as
"dbc_contract_operator_at_index" (while it cannot of course contain "[]" as
if "dbc_contract_operator[]_index" was used) -- contracts for operators are
supported by the macro-based API as well.

The contract class is used to specify the function contract:
a) It implements the DBC call semantic -- in call().
b) It specifies preconditions -- in require().
c) It specifies postconditions -- in ensure().
 d) It expects invariants to be specified by a friend non-member function
named DBC_INVARIANT_FUN_NAME.
e) It supports subcontracting via the second template parameter of
dbc::fun::mem<> (more details below).

*NOTE* It was a requirement to support contracts for overloaded and operator
functions.

(8) dbc::fun<> is used to specify non-member function contracts and
dbc::fun::mem<> is used for specify member function contracts. The second
template parameter of dbc::fun::mem<> is optional, it needs to be specified
only when subcontracting, and it is the contract class of the base class
member function from which this contract is subcontracted (in this example,
RelaxedNameList::dbc_constract_put_name subcontracts from
NameList::dbc_contract_put_name).

*NOTE* It was a requirement to support subcontracting with little to no
extra coding for the programmers.

(9) require() checks preconditions which pass if this function does not
throw, terminate, or exit. Arguments are:
    self is a constant reference to *this passed to call() -- see (3).
    name is a constant reference to the name argument passed to call() --
see (3).

self and name are constant references so precondition checking code
cannot (easily) change object and/or argument state. Similar constant
references are used when passing object and arguments to postcondition and
invariant checking code (see ensure() and DBC_INVARIANT_FUN_NAME() below).

*NOTE* It was a requirement to prevent precondition, postcondition, and
invariant checking code from (easily) altering object and/or argument state.

(10) ensure() checks postconditions which pass if this function does not
throw, terminate, or exit. This function's arguments are similar to the ones
of require() -- see (9). However, here dbc::post<> is used to support "old"
in postconditions but only for the types specified copyable by the
programmers.

dbc::post<T> has a constant member variable ".now" to access the
current value of the relative argument (e.g., self.now is the current value
of the object). dbc:: post<dbc::copyable<T> > is a template specialization
that in addition to ".now" also has a constant member variable ".old"
to access the value of the relative argument _before_ the execution of the
function body (e.g., self.old is the value of the object before the body
execution). For dbc::post<dbc::copyable<T> >, T must have a copy constructor
and its value before body execution is automatically copied by this library
at run-time (therefore adding the copy operation run-time overhead but only
for arguments of types marked dbc::copyable<> by the programmers).

*NOTE* It was a requirement to support "old" in postconditions but only for
types with a copy constructor and leaving the option to programmers to
specify for which arguments "old" (and the relative copy operation run-time
overhead) should apply.

(11) This is the body code (last code block passed to the macro-based API).
It is the definition of the member function as it would have been written if
there were not contracts! It can be the actual definition { ... }, the ';'
to separate definition from declaration, '= 0;' to support contracts for
pure virtual functions, etc (all the usual C++ expressions that can follow a
member function declaration can be used).

*NOTE* It was a requirement to support contracts (and subcontracting) for
pure virtual functions. It was also a requirement to allow for separating
body definition from contract declarations.

(12) This restores original access level (public in this case).

(13) The function named by the expansion of the DBC_INVARIANT_FUN_NAME macro
checks the invariants which pass if this function does not throw, terminate,
or exit. This function has the special indicated by the macro
DBC_INVARIANT_FUN_NAME so the library knows how to call it -- "#define
DBC_INVARIANT_FUN_NAME dbc_invaraint_". This function's arguments are
similar to ones of require() -- see (9).

(14) This is what the DBC_BODY() macro does. Note that contracts only affect
the class declaration (.hpp files). The only change to the class definition
instead is the wrapping of the member function names within the DBC_BODY()
macro.

*NOTE* It was a requirement to localize all contracts with the class
declaration (as contracts are part of the class specification) and to leave
the class definition essentially unchanged.

Cheers,
Lorenzo