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-18 14:16:06

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_at_[hidden]> 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