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