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

[Lorenzo Caminiti]

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
_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost

[Neil Groves-3]

On Sat, Oct 17, 2009 at 8:04 PM, Lorenzo Caminiti <lorcaminiti@...>wrote:

> Hello all,
>
> Is there any interest in a library that supports Design By Contract
> (DBC) for C++?
>
>
Yes, a Boost version of DbC would be fantastic. I have been using a
half-baked macro solution for years, and would be delighted to assist.



> All DBC features of the Eiffel programming language are supported by
> this library, among others:
> 2) Subcontracting for derived classes.
>


Have you managed to correctly test the derived classes class invariants in
the destructor and constructor?
Is it possible to alter the behaviour when a contract is violated? My
experience shows that it is better to allow more flexibility than simply
terminating the program. I often use exceptions and an exception handling
strategy that allows various objects to be disposed and other objects
invariants to be maintained followed by continuation. This is vital in some
cases where total program termination would be dangerous e.g. flight control
systems. This, of course, introduces problems with how one handles
violations from destructors in particular.
Does your constructor precondition checking occur before initialisation
through the member initialisation list?
Does your invariant checking mandate the use of a virtual function?

3) Use of "old" in postconditions.

>
> EXAMPLE
>
> 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_);
>    })
>

While I appreciate the intense difficulty in putting these features into C++
the DBC_CONSTRUCTOR and DBC_INHERIT_OBJECT look so foreign that I wonder if
the advantages outweigh the disadvantages of other design alternatives such
as requiring the discipline of the developer to call base functions. If you
are managing to maintain Liskov substitution principle automatically though,
then I might be convinced that this is worth the strange syntax.

<snip>
</snip>

   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");
>    })
>

The DBC_INVARIANT checking with the ability to add instance information is
excellent and often neglected. This hugely reduces time to defect
resolution. I assume that the same facility exists in the pre and
post-condition assertions.


> };
>
>
<snip>
</snip>

As you can tell, I am extremely keen for a solution that can be standardised
and peer reviewed. I hope you have the time to answer my questions.

Best wishes,
Neil Groves
_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost

[Lorenzo Caminiti]

Hello Neil,

Thank you for your reply and please see my answers below (some points
would require more discussion).

On Sun, Oct 18, 2009 at 4:44 AM, Neil Groves <neil@...> wrote:
> Have you managed to correctly test the derived classes class invariants in
> the destructor and constructor?

Yes, I tested constructor and destructor contracts to the best of my
knowledge but (in general) a peer review of this library is yet to be
done to confirm its correctness.

At the moment, this library has been tested against:
1) All DBC examples from "Object Oriented Software Construction", B.
Meyer, 1997 (not too many examples actually, all in Eiffel).
2) All examples from "Design by Contract, by Example", R. Mitchell, J.
McKim, 2002 (quite a few examples in Eiffel for every DBC feature,
including somewhat complex examples of subcontracting).
3) Specific test programs I have written (for subcontracting, I have
tested multiple inheritance and up to 3-4 levels of derived classes).
4) A real-world software development project (which did not require
much subcontracting but it used about 300 different classes).
If you have specific code examples for which subcontracting would
present a challenge, I would be happy to write contracts using this
library for your examples and use them as test programs.

> Is it possible to alter the behaviour when a contract is violated? My
> experience shows that it is better to allow more flexibility than simply
> terminating the program. I often use exceptions and an exception handling
> strategy that allows various objects to be disposed and other objects
> invariants to be maintained followed by continuation. This is vital in some
> cases where total program termination would be dangerous e.g. flight control

Yes, when using DBC_ASSERT and DBC_ASSERT_STREAM programmers can chose
to throw, terminate, or exit. This is inline with your comment above
as well as a requirement from "Proposal to add Design by Contract to
C++", T. Ottosen, C++ Standards Committee Paper N1613, 2004.

1) The default behavior of DBC_ASSERT is to throw but that can be
changed by the programmers to terminate or exit via a library
configuration macro DBC_CONFIG_... (similar to the configuration
macros BOOST_PP_CONFIG_... of Boost.Preprocessor).

2) In addition on changing the default behavior of DBC_ASSERT,
programmers can specify for each DBC_ASSERT_STREAM if to throw,
terminate, or exit (using a stream modifier syntax).

DBC_ASSERT(false, "always fails"); // This takes the default behavior,
configurable (throw is the default configuration of the default
behavior).
DBC_ASSERT_STREAM(false, "always fails", err << "asserted false"); //
This takes the default behavior, configurable (same as using
DBC_ASSERT but this can specify a more verbose error message).
DBC_ASSERT_STREAM(false, "always fails", err << "asserted false" <<
dbc::raise<std::logic_error>()); // This throws a user defined
exception (std::logic_error in this example).
DBC_ASSERT_STREAM(false, "always fails", err << "asserted false" <<
dbc::terminate()); // This terminates.
DBC_ASSERT_STREAM(false, "always fails", err << "asserted false" <<
dbc::exit(2)); // This exits with code 2.

Also, programmers can selectively enable or disable runtime assertion
checking based on their behavior. For example, programmers can use a
library configuration macro to say "do not check any assertion that
exits the program" (this was also a requirement from Ottosen2004 cited
above).

3) Finally, this library allows for any legal C++ code to be
programmed in the preconditions, postconditions, and invariants code
blocks. Therefore, programmers can do what they wish in case the use
of DBC_ASSERT or DBC_ASSERT_STREAM does not serve their purposes.
(However, not using DBC_ASSERT or DBC_ASSERT_STREAM is not recommended
and it will limit DBC functionalities like selective runtime check
enabled/disable, automatically generated contract documentation for
doxygen, etc.)

> systems. This, of course, introduces problems with how one handles
> violations from destructors in particular.

True. This was an interesting issue to deal with together with the C++
STL exception safety requirements.

Ottosen2004 suggests that invariants should be checked before
executing the destructor body:

    Destructor-Call := {Inv} Body {}

Ottosen2004 also requires destructors to never throw (because of STL
exception safety requirements). Ottosen2004 suggests the invocation of
a dbc::broken_destructor_invariant() function pointer in case of a
destructor contract violation. By default, the
dbc::broken_destructor_invariant() function pointer executes a
function that terminates but the user can change the function pointer
to execute a user-defined function that takes a different action (same
as std::terminate()). This is what this library implements.

More interesting (and challenging) was the case of a destructor
contract violation during stack unwinding due to a previous contract
violation that resulted in throwing an exception. This is working now
(as far as I could test it) but I would require accurate review.

> Does your constructor precondition checking occur before initialisation
> through the member initialisation list?

No, preconditions are checked *after* member initialization.

I had no option to check before member initialization. Meyer1997
defines DBC for constructors as:

    Constructor-Call := "{Defaults AND Pre} Body {Inv AND Post}"
    Where: "Defaults" indicates that members have been initialized to
their default values and it plays the role of the C++ constructor
member initialization list; AND is evaluated in short-circuit.

Therefore, Meyer1997 requires preconditions to be checked after member
initialization as this library does. However, if I had the option to
do differently, I might have done so...

(Furthermore, I faced an important limitation in dealing with member
initialization when separating declaration and definition of
constructors. I was only able to implement a work around for this
limitation which could be address more properly in case the future C++
standard were to accept the delegating constructor proposal...
illustrating this specific issue would require a separate
conversation.)

> Does your invariant checking mandate the use of a virtual function?

Can you please clarify the question: Which functions shall be virtual?
(For example, Stack4::remove() is not virtual...)

> While I appreciate the intense difficulty in putting these features into C++
> the DBC_CONSTRUCTOR and DBC_INHERIT_OBJECT look so foreign that I wonder if
> the advantages outweigh the disadvantages of other design alternatives such
> as requiring the discipline of the developer to call base functions. If you

I agree, the foreign looking syntax of the macro-based API is a clear
disadvantage (at the end, it is all standard C++ but it looks very
uncommon). I got used to it now. To other programmers, it usually
takes about 1 week of using the library to became familiar with this
syntax. However, your class declarations (typically the .hpp files)
will always look "different" (the foreign syntax does NOT propagate to
the class definitions especially if they are in separate .cpp files).
Furthermore, there is only a limited amount of compile-time error
checking (using Boost.MPL static assertions) that this library can do
to make sure programmers use this syntax correctly (in the other
cases, mysterious complier errors appear).

*** To me, this is a key question for Boost programmers: IS THIS C++
SYNTAX TOO FOREIGN LOOKING OR DIFFICULT TO USE TO BE ACCEPTABLE? ***

Macros are kind of necessary so compilation (not just runtime
checking) of the contract can be turned off. This is important so if
you are releasing software that only checks preconditions (after you
tested also with invariants and postconditions enabled) you can
compile only the preconditions minimizing both the runtime overhead
and the size of your object files.

For example, instead of DBC_INHERIT_OJBECT, programmers do have the
option to write:

template<typename T>
class Stack4
#ifdef DBC // "DBC" is #defined by this library when DBC compilation
and checking is enabled.
    : dbc::object<Stack4<T> >
#endif // DBC
    {
public:
    ...

But to me this code is more confusing and error prone than using the
DBC_INHERIT_OBJECT macro.

Similarly, programmers can use the library template dbc::fun::constr<>
to write the constructor contract code directly avoiding the use of
the strange looking DBC_CONSTRUCTOR() macro but that code looks even
more polluted than the one using dbc::object<> above...

In short, the macros are not required by this library but their use
makes the programmers' life so much easier... Without adding keywords
to the language or using an external preprocessor (not the C++ one) to
translate special comments or similar text into code, I was not able
to find any alternative to these foreign-looking macros in order to
save the programmers from writing a lot of setup code around the
contracts polluted with #ifdef, etc. (It was a requirement for me to
only use standard C++ and its preprocessor, no external tools.)

> are managing to maintain Liskov substitution principle automatically though,
> then I might be convinced that this is worth the strange syntax.

When subcontracting, programmers only need to specify the base class
(note there could be multiple base classes because of C++ multiple
inheritance). The library will automatically check the base contract
together with the derived class contract as indicated by Meyer1997
(and satisfying Liskov substitution principle):

    Function-Call := {Inv [AND Base-Inv] AND Pre [OR Base-Pre]} Body
{Inv [AND Base-Inv] AND Post [AND Base-Post]}
    Where: [...] is present only when subcontracting; AND/OR are
evaluated in short-circuit.

Here is how the code looks like when subcontracting -- note the use of
DBC_BASE() in RelaxedNameList::put() contract. (This example was
presented for Eiffel in Mitchell2002.)

/** Name list with no duplicates. */
class NameList DBC_INHERIT_OBJECT(NameList) {
public:
    virtual void put(const std::string& name)
    DBC_MEM_FUN( (public) (virtual) (void) DBC_COPYABLE(NameList)
            (put)( (const std::string&)(name) ), {
        // This precondition does not allow for duplicated names in the list.
        DBC_ASSERT_STREAM(!self.has(name), "not in list",
                err << "name '" << name << "' already in list");
    }, {
        if (!self.old.has(name.now))
            DBC_ASSERT_STREAM(self.now.has(name.now),
                    "if require passed, in list",
                    err << "name '" << name.now << "' not in list");
        if (!self.old.has(name.now))
            DBC_ASSERT(self.now.count() == (self.old.count() + 1),
                    "if was not in list, count increased");
    }, ;)
    ...
};

/** Name list with duplicates. */
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) //
Subcontracting via DBC_BASE().
            (put)( (const std::string&)(name) ), {
        // This precondition in OR with the base one allows for
duplicated names in the list.
        DBC_ASSERT_STREAM(self.has(name), "in list",
                err << "name '" << name << "' not in list");
    }, {
        if (self.old.has(name.now))
            DBC_ASSERT(self.now.count() == self.old.count(),
                    "if in list, count unchanged");
    }, ;)
    ...
};

> The DBC_INVARIANT checking with the ability to add instance information is
> excellent and often neglected. This hugely reduces time to defect
> resolution. I assume that the same facility exists in the pre and
> post-condition assertions.

Can you please describe in more detail what you mean by the "ability
to add instance information"? Preconditions and postconditions also
have access to the object instance "self" (as constant reference so
they cannot _easily_ modify the object state).

> As you can tell, I am extremely keen for a solution that can be standardised
> and peer reviewed. I hope you have the time to answer my questions.
>
> Best wishes,
> Neil Groves
> _______________________________________________
> Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
>

Cheers,
Lorenzo
_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost

[Gottlob Frege]

>
> *** To me, this is a key question for Boost programmers: IS THIS C++
> SYNTAX TOO FOREIGN LOOKING OR DIFFICULT TO USE TO BE ACCEPTABLE? ***
>

Yes. (Sorry.)
Tony
_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost

[Thomas Klimpel]

Gottlob Frege wrote:
> Lorenzo Caminiti wrote:
> > *** To me, this is a key question for Boost programmers: IS THIS C++
> > SYNTAX TOO FOREIGN LOOKING OR DIFFICULT TO USE TO BE ACCEPTABLE? ***
>
> Yes. (Sorry.)

Doesn't Boost.Parameter also uses a foreign looking syntax? But I admit that "DBC_MEM_FUN" is a bit cryptic. How about BOOST_DBC_MEMBER_FUNCTION?

Regards,
Thomas
_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost

[Gottlob Frege]

On Sun, Oct 18, 2009 at 6:01 PM, Thomas Klimpel
<Thomas.Klimpel@...> wrote:

> Gottlob Frege wrote:
>> Lorenzo Caminiti wrote:
>> > *** To me, this is a key question for Boost programmers: IS THIS C++
>> > SYNTAX TOO FOREIGN LOOKING OR DIFFICULT TO USE TO BE ACCEPTABLE? ***
>>
>> Yes. (Sorry.)
>
> Doesn't Boost.Parameter also uses a foreign looking syntax? But I admit that "DBC_MEM_FUN" is a bit cryptic. How about BOOST_DBC_MEMBER_FUNCTION?
>
> Regards,
> Thomas

Yes, Boost.Parameter is a bit odd as well.  And it makes me hesitate
to use it - not avoid it, but hesitate - ie depends on where/how it is
used.  Yet, in general, I like DSEL (domain-specific embedded
languages), and have written a few.
But here's the thing:

   they are **domain-specific**

This, for me at least, makes a big difference.  I don't mind seeing
some strangeness within a certain domain or to solve a particular
problem.  But when the augmented language is NOT domain-specific, and
instead is used all over your code, then I start thinking that maybe
we should just be using a different language.

Maybe that's just me.  And really, I'm just realizing this 'criteria'
of mine right now.  It is not the only factor I use when looking at
macros/DSELs/libraries/coding-standards/idioms/etc, but thinking back
to things I've liked/disliked, it seems to be important to me.

Hope that makes sense, even though I realize I didn't really explain
the difference or give examples, etc.

Just my opinion,
Tony

P.S. I also just hate macros.  Maybe for the same reason.
_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost

[Paul A. Bristow-2]

> -----Original Message-----
> From: boost-bounces@... [mailto:boost-bounces@...] On
Behalf Of
> Gottlob Frege
> Sent: Monday, October 19, 2009 8:30 AM
> To: boost@...
> Subject: Re: [boost] [dbc] Interest in Design By Contract for C++?
>
> >> Lorenzo Caminiti wrote:
> >> > *** To me, this is a key question for Boost programmers:

> >> > IS THIS C++ SYNTAX TOO FOREIGN LOOKING OR DIFFICULT TO USE TO BE
ACCEPTABLE? ***

Acronymitis is a serious problem for me ;-(

DBC_ everywhere just looks very nasty.

One could learn to live with it, but the number of brackets required to use the
macros adds insult to injury.

And the syntax of the macros looks less than intuitive (as always with macros).

If this intended to be a Boost -only library, then macros should start with
BOOST_, but that would only increase the problem of too long names that take too
long to type.

If it is for general use, I would prefer something Acronym-Free, perhaps like

DESIGN_INHERIT_OBJECT, DESIGN_MEMBER_FUNCTION ...

Sorry - but I'm sure you have been so busy grappling with the difficult macros
to consider the 'aesthetics' ;-)

Paul


---
Paul A. Bristow
Prizet Farmhouse
Kendal, UK   LA8 8AB
[phone], mobile [phone]
pbristow@...







_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost

[Lorenzo Caminiti]

Hello all,

<Thomas.Klimpel@...> wrote:
>> Lorenzo Caminiti wrote:
>> > *** To me, this is a key question for Boost programmers: IS THIS C++
>> > SYNTAX TOO FOREIGN LOOKING OR DIFFICULT TO USE TO BE ACCEPTABLE? ***
>
> Doesn't Boost.Parameter also uses a foreign looking syntax? But I admit that "DBC_MEM_FUN" is a bit cryptic. How about BOOST_DBC_MEMBER_FUNCTION?

Yes, as Thomas indicated, Boost.Parameter already uses a foreign
looking syntax. That essentially answers my question: While the
necessity to introduce a macro-based foreign looking syntax like the
one of this library should be carefully considered, I do not think
Boosters will reject it in principle.


SYNTAX

1) I knew of the existence of Boost.Parameter but I never used it so I
did not know its API. After Thomas' comment, I have studied
Boost.Parameter API and its documentation. The Boost.Parameter
macro-based foreign looking syntax is actually very similar to one of
this library: Boost.Preprocessor sequences are used to allow the
macros to generate function signatures with parameter names/types,
return types, etc; There is a BOOST_PARAMETER_MEMBER_FUNCTION,
BOOST_PARAMETER_CONSTRUCTOR, etc similarly to DBC_MEM_FUN,
DBC_CONSTRUCTOR, etc.

2) In addition, other Boost libraries like Boost.Test (great library
which I use every day) and Boost.TypeOf rely heavily on macros (even
if in a contexts different from the one of this library and
Boost.Parameter). Therefore, I think the use of macros (while always
best avoided), it is accepted by Boosters when necessary.

"The first rule about macros is: Don't use them unless you have to.
Almost every macro demonstrates a flow in the programming language, in
the program, or in the programmer.", The C++ Programming Language, B.
Stroustrup, 1997. This library uses macros to overcome a programming
language limitation extending C++ with DBC features. Languages like
Eiffel have built-in language support for DBC; Other programming
languages like Java and Ada use external pre-processing tools to
support DBC (but that's cheating...).

Gottlob Frege wrote:
>  they are **domain-specific**
> This, for me at least, makes a big difference.  I don't mind seeing
> some strangeness within a certain domain or to solve a particular
> problem.  But when the augmented language is NOT domain-specific, and
> instead is used all over your code, then I start thinking that maybe
> we should just be using a different language.

3) I also understand the concern expressed by Tony that the "DSEL"
syntax of this library has a domain that extends to all your class
*declarations* (or at least to all the ones for which you need to
write contracts) -- that is a pretty large domain... I think, at the
end designers/programmers will have to judge if the complexity added
by the macro syntax is worth the benefits of DBC for their specific
application -- but using Eiffel instead of C++ might not be a
realistic option for some (most?) applications.

In addition, I would like to stress out that the foreign looking macro
syntax only applies to the class declarations and NOT to their
definitions -- therefore, only your .hpp files will contain the
foreign looking macros, while your .cpp files will essentially remain
unchanged.


NAMING

While my question above was not directly concerned with this library
current naming conventions, quite a few comments were made on naming.
I think that means that properly chosen names could help making the
macros less cryptic (even if they will still retain the foreign
looking preprocessor-sequence syntax). In general, I will be more than
happy to change the library names to fully comply with Boost
guidelines and to be as clear as possible to Boosters.

1) Yes, if this library were to become a Boost library, all macro
names will have to start with "BOOST_" (and all library code will have
to be included in the "boost::" namespace).

2) Yes, Boost usually fully spells all symbols so MEM_FUN should be
MEMBER_FUNCTION, and same story for any other symbol of this library
that is not fully spelled. (I try to only use abbreviations already
used by the STL, like MEM_FUN similar to the std::mem_fun binder but I
am also happy to fully spell all symbols.)

3) The "DBC_BASE(type)" and "DBC_COPYABLE(type)" macros could be
replaced by "(inherit)(type)" and "(copyable)(type)" if that made the
macro syntax more clear (this will then be similar to the keywords
"optional" and "required" introduced by the Boost.Parameter macro
syntax). With a bit more work in the library implementation, I think
it might be possible to remove the need for DBC_INHERIT_OBJECT and
DBC_MULTI_INHERIT_OBJECT (I will have to look at the details of
this...).

On Mon, Oct 19, 2009 at 7:59 AM, Paul A. Bristow
<pbristow@...> wrote:
> Acronymitis is a serious problem for me ;-(
> DBC_ everywhere just looks very nasty.

4) DBC (actually "DbC"(TM) to be precise, as indicated by Neil) is a
well recognize industry acronym for "Design by Contract"(TM). However,
there might be trademark concerns in using this acronym (see
http://en.wikipedia.org/wiki/Design_by_contract) and programmers have
been using Programming by Contracts (PbC) or Contract Programming (CP)
instead. The use of these other, much less know, acronyms will only
increase Paul's concern above... In my opinion, if DBC is not to be
used than "Contract" will be the best alternative.


NAMING OPTIONS

a) Use "DBC" (similar to Boost.MPL, Boost.CRC, etc)
Library: Boost.DBC
Namespace: boost::dbc
Macros: BOOST_DBC_CONSTRUCTOR, BOOST_DBC_DESTRUCTOR,
BOOST_DBC_MEMBER_FUNCTION, etc

b) Use "Contract" (similar to Boost.Parameter, Boost.Test, etc)
Library: Boost.Contract
Namespace: boost::contract
Macros: BOOST_CONTRACT_CONSTRUCTOR, BOOST_CONTRACT_DESTRUCTOR,
BOOST_CONTRACT_MEMBER_FUNCTION, etc

I am equally happy with either option a) or b).


EXAMPLE OF b)

This the NameList example I presented in a previous email reworked to
use naming convention b). It also shows that the foreign looking macro
syntax does NOT affect your .cpp files when function definitions are
separated from their declarations.

// File: RelaxedNameList.hpp (declarations with foreign looking macros).

#include <boost/contract.hpp> // This library, if added to Boost as in
option b).

class RelaxedNameList: public NameList
        // Maybe the "..._INHERIT_OBJECT()" macros can be removed...
not sure yet.
        BOOST_CONTRACT_MULTI_INHERIT_OBJECT(RelaxedNameList) {
public:
    void put(const std::string& name)
    BOOST_CONTRACT_MEMBER_FUNCTION( (public) (void)
            // Using "copyable" and "inherit" instead of
"..._COPYABLE()" and "..._BASE()" macros.
            (copyable)(RelaxedNameList) (inherit)(NameList) //
Subcontracting (inherit) from NameList::put.
            (put)( (const std::string&)(name) ), {
        // This preconditions (in OR with the base preconditions
allowing for duplicated names in the list).
        BOOST_CONTRACT_ASSERT_STREAM(self.has(name), "in list",
                err << "name '" << name << "' not in list");
    }, {
        // This postconditions (in AND with base postconditions).
        if (self.old.has(name.now))
                BOOST_CONTRACT_ASSERT(self.now.count() == self.old.count(),
                        "if in list, count unchanged");
    }, ; /* Body: ";" to separate definition from declaration. */ )

    ...

private:
    BOOST_CONTRACT_INVARIANT(RelaxedNameList, {
        // Invariants (in AND with base invariants, no additional
invariant here).
    })
};

// EOF


// File: RelaxedNameList.cpp (definitions, with NO foreign looking
macro a part from BOOST_CONTRACT_BODY).

#include "RelaxedNameList.hpp"

void RelaxedNameList::BOOST_CONTRACT_BODY(put)(const std::string& name) {
    ... // This function implementation.
}

...

// EOF


Thank you all for your comments so far. I will follow up with a couple
of more technical emails illustrating some of the library internal
mechanisms and comparing this library with DBC support from other
languages, libraries, and proposals.

Cheers,
Lorenzo
_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost

[Lorenzo Caminiti]

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
_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost

[Lorenzo Caminiti]

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.
_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost