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

Subject: [boost] [dbc] Interest in Design By Contract for C++?
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2009-10-17 15:04:18

Hello all,

Is there any interest in a library that supports Design By Contract
(DBC) for C++?

All DBC features of the Eiffel programming language are supported by
this library, among others:
1) Optional compilation and runtime checking of preconditions,
postconditions, and invariants.
2) Subcontracting for derived classes.
3) Use of "old" in postconditions.
4) Automatic contract documentation (integrated with doxygen or similar tools).

EXAMPLE

This is part of the Stack4 DBC example presented for Eiffel in the
book "Object Oriented Software Construction", B. Meyer, 1997. It has
been coded for C++ using this library.

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

template<typename T>
class Stack4 DBC_INHERIT_OBJECT(Stack4<T>) {
public:
    Stack4(const int& n): capacity_(0), count_(0), representation_()
    DBC_CONSTRUCTOR( (private) (template)(Stack4)( (const int&) (n) ), {
        // Constructor preconditions.
        DBC_ASSERT(n >= 0, "non negative capacity");
    }, {
        // Constructor postconditions.
        DBC_ASSERT(self.now.capacity() == n.now, "capacity set");
        DBC_ASSERT(self.now.empty(), "is empty");
    }, {
         // Constructor body.
        capacity_ = n;
        representation_.resize(capacity_);
    })

    virtual ~Stack4()
    DBC_DESTRUCTOR( (public) (virtual) (template)(Stack4)(), {
        // Destructor body (do nothing).
    })

    void remove()
    DBC_MEM_FUN( (public) (void) (template)DBC_COPYABLE(Stack4) (remove)(), {
        // Member function preconditions.
        DBC_ASSERT(!self.empty(), "not empty");
    }, {
        // Member function postconditions.
        DBC_ASSERT(!self.now.full(), "not full");
        DBC_ASSERT(self.now.count() == (self.old.count() - 1),
                "count decreased");
    }, {
        // Member function body.
        --count_;
    })

    ... // The rest of the Stack4 class.

private:
    int capacity_;
    int count_;
    std::vector<T> representation_;

    DBC_INVARIANT(Stack4, {
        DBC_ASSERT(self.count() >= 0, "count non negative");
        DBC_ASSERT_STREAM(self.count() <= self.capacity(),
                "count no greater than capacity",
                err << "count " << self.count() << " bounded by capacity "
                << self.capacity());
        DBC_ASSERT(
                self.capacity() == int(self.representation_.capacity()),
                "capacity consistent with vector capacity");
        DBC_ASSERT(self.empty() == (self.count() == 0),
                "empty when no elements");
        if (self.count() > 0) DBC_ASSERT(
                self.representation_.at(self.count() - 1) == self.item(),
                "if positive count, item at top");
    })
};

Example Notes:
a) The somewhat strange syntax of the macro-based API (i.e.,
DBC_CONSTRUCTOR(), DBC_DESTRUCTOR(), and DBC_MEM_FUN()) uses a C++
preprocessor sequence of tokens "(public) (void) (template) ..." (this
library internally uses Boost.Preprocessor to implement these macros).
This library also provides a code-based API (dbc::fun::constr<>,
dbc::fun::destr<>, and dbc::fun::mem<>) that can be used instead of
the macro-based API but more setup code needs to be written by the
programmers.
b) This library also internally uses Boost.MPL mainly for typetraits,
to support "old" in postconditions but only for types marked
DBC_COPYABLE(), and for static assertions checking for library
missuses (e.g., incorrect preprocessor sequence of tokens passed to
the macro-based API).
c) This library requires contracts to be written together with the
class declaration (as contracts are part of the class specification).
The class definition (function body) instead can either be written
together with the contracts in the class declaration (like in the
example above) or it can be written separately from the class
declaration (i.e., this library maintains for function bodies the same
C++ feature that allows to separate function's declaration and
definition).

Cheers,
Lorenzo