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-28 22:35:02

Hello all,

Below I am comparing DBC features between this C++ library, Eiffel,
the D programming language, and the C++ Standard Committee proposal
for adding DBC to C++ [Ott04].

Does anyone know of other libraries offering Eiffel-like DBC support for C++?

As far as I know, there is no publicly available library for C++ that
supports all DBC features offered by Effiel. Existing DBC tools for
C++ lack of support for either "old" in postconditions,
subcontracting, automatic contract documentation, or a combination of
the above. This library provides all Eiffel DBC features for C++ (and
it does not require external preprocessing tools, just the C++
preprocessor).

Thank you.

Lorenzo

DBC FEATURE COMPARISON

[Ott04] ["C++ Std. Prop." below] T. Ottosen, Proposal to add Design by
Contract to C++. C++ Standards Committee Paper N1613, 2004.
http://www.open-std.org/JTC1/SC22/WG21/docs/papers/2004/n1613.pdf
(Eiffel and D have built-in language support for DBC.)

DBC keywords
    This Library: No keyword -- it is a library. Code-based API (no
keywords) follow Eiffel names: require(), ensure(), DBC_BODY(), .old
(and .now), and DBC_INVARIANT().
    Effiel: require, ensure, do, require else, ensure then, old,
invariant, and result.
    D: in, out, body, invariant, and assert.
    C++ Std. Prop.: in, out, do, invariant, and return.

On condition violation
    This Library: Throw (by default), terminate, or exit. Programmer
can select action on violation using DBC_ASSERT() and
DBC_ASSERT_STREAM().
    Eiffel: Throw exception.
    D: Throw exception.
    C++ Std. Prop.: Terminate (by default), might throw or exit.

Return value evaluation
    This Library: Yes. result argument of ensure() (only if
postconditions compiled in object code).
    Eiffel: Yes, result keyword.
    D: No.
    C++ Std. Prop.: Yes, return keyword.

Expression copying in postconditions ("old")
    This Library: Yes. For object and function arguments declared
DBC_COPYABLE() or dbc::copyable, accessed via .old (only if
postconditions compiled in object code and requires type to have copy
constructor).
    Eiffel: Yes, old keyword.
    D: No.
    C++ Std. Prop.: Yes, in keyword.

Subcontracting
    This Library: Yes. Use DBC_BASE() or B template parameter of
dbc::fun::mem<> (but derived class programmer can decide to
subcontract or not, recommended to always subcontract).
    Eiffel: Yes.
    D: Yes.
    C++ Std. Prop.: Yes.

Assertion naming
    This Library: Yes. A string passed to DBC_ASSERT() and DBC_ASSERT_STREAM().
    Eiffel: Yes.
    D: No.
    C++ Std. Prop.: No.

Arbitrary code in contracts
    This Library: Yes. But recommended to keep contract code simple,
ideally limit it to a list of assertions.
    Eiffel: No.
    D: Yes.
    C++ Std. Prop.: No.

Contracts access level
    This Library: Any. Preconditions, postconditions, and invariants
can access any class member public, protected, or private. But
recommended to write contracts using public members as much as
possible. In particular, preconditions should only use public members
otherwise the caller will not be able to make sure the contract holds
before invoking the function...
    Eiffel: Preconditions cannot access public members (to avoid
contracts that cannot be checked by the caller).
    D: Any.
    C++ Std. Prop.: Any.

Contract for abstract functions
    This Library: Yes. When body is defined pure virtual by "= 0;".
    Eiffel: Yes.
    D: No.
    C++ Std. Prop.: Yes.

Code ordering
    This Library: Preconditions > postconditions > body (for
macro-based API only).
    Eiffel: Order: Preconditions > body > postconditions.
    D: Order: Preconditions > postconditions > body.
    C++ Std. Prop.: Preconditions > postconditions > body.

Static assertions
    This Library: Yes. Use C++ metaprogramming (e.g., the Boost.MPL library).
    Eiffel: No.
    D: Yes.
    C++ Std. Prop.: Yes.

Prevent contract side-effects
    This Library: Yes. Use constant code block, constant object self,
constant function arguments, and constant result to limit unintended
contract side side-effects.
    Eiffel: Yes.
    D: No.
    C++ Std. Prop.: No.

Contracts removable from object code
    This Library: Yes. Compilation and checking of preconditions,
postconditions, invariants, and any of their combination can be
enabled or disabled using the DBC_CHECK_... macros.
    Eiffel: Yes.
    D: Yes.
    C++ Std. Prop.: Only default assertions.

Check invariants
    This Library: At end of constructors, at beginning and end of
member functions, and at beginning of destructor (if programmer
specifies contracts for those). E.g., programmer may omit contract for
all private member functions so their calls will not check invariants.
Furthermore, invariant checking in destructor is disabled during stack
unwinding because of an unhandled exceptions (as contracts themselves
can throw).
    Eiffel: At end of constructors, at beginning and end of public
member functions.
    D: At end of constructors, at beginning and end of public member
functions, and at beginning of destructor.
    C++ Std. Prop.: At end of constructors, at beginning and end of
public member functions, and at beginning of destructor.

Disabling assertion checking within assertions
    This Library: Yes. To prevent infinite recursion when checking contracts.
    Eiffel: Yes.
    D: No.
    C++ Std. Prop.: Yes.

In nested function calls
    This Library: Disable invariants only. To prevent infinite
recursion when checking contracts.
    Eiffel: Disable all assertions.
    D: Disable nothing.
    C++ Std. Prop.: Disable invariants only.

Concurrency
    This Library: Not yet. To implement this similarly to Eiffel
(i.e., making this library thread-safe and supporting waiting
conditions...).
    Eiffel: Yes (implements waiting conditions).
    D: No.
    C++ Std. Prop.: No.

Automatic contract documentation
    This Library: Yes. doxygen is used by default (see DBC_CONFIG_DOC_...).
    Eiffel: Yes (contracts are part of the class' "short form").
    D: No with existing documentation tools.
    C++ Std. Prop.: No with existing documentation tools.