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