[dbc] Interest in Design By Contract for C++?
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
On Sat, Oct 17, 2009 at 8:04 PM, Lorenzo Caminiti <lorcaminiti@gmail.com>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
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@grovescomputing.com> 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
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
On Sun, Oct 18, 2009 at 6:01 PM, Thomas Klimpel <Thomas.Klimpel@synopsys.com> 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.
-----Original Message----- From: boost-bounces@lists.boost.org [mailto:boost-bounces@lists.boost.org] On Behalf Of Gottlob Frege Sent: Monday, October 19, 2009 8:30 AM To: boost@lists.boost.org 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 +44 1539 561830, mobile +44 7714330204 pbristow@hetp.u-net.com
Hello all, <Thomas.Klimpel@synopsys.com> 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@hetp.u-net.com> 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
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
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.
participants (5)
-
Gottlob Frege -
Lorenzo Caminiti -
Neil Groves -
Paul A. Bristow -
Thomas Klimpel